### ACL2-PC::USE

(atomic macro)
` `

use a lemma instance
Major Section: PROOF-CHECKER-COMMANDS

Example:
(USE true-listp-append
(:instance assoc-of-append (x a) (y b) (z c)))
-- Add two top-level hypotheses, one the lemma called
true-listp-append, and the other an instance of the lemma called
assoc-of-append by the substitution in which x is assigned a, y
is assigned b, and z is assigned c.
General Form:
(use &rest args)

Add the given lemma instances to the list of top-level hypotheses.
See hints for the syntax of `:use`

hints in `defthm`

, which is
essentially the same as the syntax here (see the example above).This command calls the `prove`

command, and hence should only be used
at the top of the conclusion.