Use a (functional instance of a) previously-proved measure theorem
See lemma-instance for a discussion of
:termination-theorem and :termination-theorem! lemma instances, and
see tthm for a related user-level query utility. Also see termination-theorem-example for simple examples of the use of
measure (termination) theorems in hints. For a related utility, see
make-termination-theorem.
