implicate

(in-package "ACL2")

(defsection std/system/implicate
  :parents (std/system/term-transformations)
  :short "Theorems about @(tsee implicate)."
  (defthm pseudo-termp-of-implicate
    (implies (and (pseudo-termp term1) (pseudo-termp term2))
      (pseudo-termp (implicate term1 term2)))))