|
|
|---|
|
|
|
|---|
(atomic macro) use a lemma instance
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
This command calls the