plist-worldp-with-formals

(in-package "ACL2")

(defsection std/system/plist-worldp-with-formals
  :parents (std/system)
  :short "Theorems about @('plist-worldp-with-formals')
          (see the ACL2 source code)."
  (defthm plist-worldp-when-plist-worldp-with-formals-cheap
    (implies (not (plist-worldp wrld))
      (not (plist-worldp-with-formals wrld)))
    :rule-classes ((:rewrite :backchain-limit-lst (0)))))