getprops

(in-package "ACL2")

(defsection std/system/geprops
  :parents (std/system)
  :short "Theorems about @('getprops') (see the ACL2 source code)."
  (defthm alistp-of-getprops
    (alistp (getprops key world-name w))))