pseudo-event-formp

(in-package "ACL2")

(defsection std/system/pseudo-event-formp
  :parents (std/system)
  :short "Theorems about @(tsee pseudo-event-formp)."
  (defthm booleanp-of-pseudo-event-formp
    (booleanp (pseudo-event-formp x)))
  (defthm pseudo-event-formp-of-cons
    (equal (pseudo-event-formp (cons a b))
      (and (symbolp a) (true-listp b)))))