prove command, and hence should only be used
at the top of the conclusion.
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.