How to use a previously-proved guard theorem

See lemma-instance for a discussion of

The following example is contrived but should get the idea across. Suppose
that the event displayed just below was previously executed, for example when
including a book. The `mbe` call generates a guard proof obligation,
but there is only one thing to know about that for this example: without the
local lemma shown, the guard proof fails for

(encapsulate () (local (defthm append-revappend (equal (append (revappend x y) z) (revappend x (append y z))))) (defun f1 (x y) (declare (xargs :guard (and (true-listp x) (true-listp y)))) (mbe :logic (append (reverse x) y) :exec (revappend x y))))

Now suppose that later, we wish to admit a function with the same guard and
body. Since the lemma

(defun f2 (x y) (declare (xargs :guard (and (true-listp x) (true-listp y)) :guard-hints (("Goal" :use ((:guard-theorem f1)))))) (mbe :logic (append (reverse x) y) :exec (revappend x y)))

See termination-theorem-example for an example use of the analogous
lemma instance type,