dumb-negate-lit

(in-package "ACL2")

(defsection std/system/dumb-negate-lit
  :parents (std/system/term-transformations)
  :short "Theorems about @(tsee dumb-negate-lit)."
  (defthm pseudo-termp-of-dumb-negate-lit
    (implies (pseudo-termp term)
      (pseudo-termp (dumb-negate-lit term)))))