		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::instantiate

Instantiate a theorem

Example:
(instantiate car-cons (x (append a b)) (y nil))
;; This will add the following hypothesis:
;; (let ((x (append a b))
;;       (y nil))
;;   (equal (car (cons x y)) x))

General Form:
(instantiate thm-name subst1 ... substk)

where each substi is an assignment of a variable used in the formula associated with thm-name to a term.

Note that the variables used in the formula associated with thm-name may be in a different package than the one you are currently in. In this case, explicitly specify the package when writing variable names in substitutions.