Use a previously-proved guard theorem
See lemma-instance for a discussion of :guard-theorem
lemma instances, as illustrated in the topic guard-theorem-example.
The function guard-theorem is a low-level system utility that returns
a translated term. It is essentially the functional version of the
gthm macro, which however returns an untranslated term. See gthm.
Verify guards efficiently by using a previous guard theorem.
- How to use a previously-proved guard theorem