		Search-engine friendly clone of the ACL2 documentation.

Lift-term

Lift pseudo-terms to the meta level.

Theorem: return-type-of-lift-term.tterm

(defthm return-type-of-lift-term.tterm
  (b* ((?tterm (lift-term term)))
    (ttermp tterm))
  :rule-classes :rewrite)

Theorem: return-type-of-lift-term-list.terms

(defthm return-type-of-lift-term-list.terms
  (b* ((?terms (lift-term-list terms)))
    (tterm-listp terms))
  :rule-classes :rewrite)