pseudo-event-form-listp

(in-package "ACL2")

(deflist pseudo-event-form-listp
  (x)
  (pseudo-event-formp x)
  :parents (std/system)
  :short (topstring "Recognize true lists whose elements all have the "
    (seetopic "pseudo-event-formp"
      "basic structure of an event form")
    ".")
  :long (topstring-@def "pseudo-event-form-listp")
  :true-listp t
  :elementp-of-nil nil
  ///
  (defthmd true-listp-when-pseudo-event-form-listp-rewrite
    (implies (pseudo-event-form-listp x) (true-listp x))))