pseudo-lambda-lemmas

(in-package "SMT")

(include-book "kestrel/utilities/system/terms" :dir :system)

(encapsulate nil
  (local (in-theory (enable pseudo-lambdap)))
  (defthm symbol-listp-of-formals-of-pseudo-lambdap
    (implies (pseudo-lambdap x)
      (symbol-listp (cadr x))))
  (defthm pseudo-termp-of-body-of-pseudo-lambdap
    (implies (pseudo-lambdap x)
      (pseudo-termp (caddr x))))
  (defthm consp-of-pseudo-lambdap
    (implies (pseudo-lambdap x) (consp x)))
  (defthm consp-of-cdr-of-pseudo-lambdap
    (implies (pseudo-lambdap x)
      (consp (cdr x))))
  (defthm consp-of-cddr-of-pseudo-lambdap
    (implies (pseudo-lambdap x)
      (consp (cddr x))))
  (defthm not-stringp-of-cadr-of-pseudo-lambdap
    (implies (pseudo-lambdap x)
      (not (stringp (cadr x))))))