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.Add the given lemma instances to the list of top-level hypotheses. See hints for the syntax of
General Form: (use &rest args)
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.