(atomic macro) use a lemma instance

(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.