If q parses into a well-typed term M, an invocation
completeInduct_on q begins a proof by complete (also known as
‘course-of-values’) induction on M. The term M should occur free in
the current goal.
FAILURE
If M does not parse into a term or does not occur free in the
current goal.
EXAMPLE
Suppose we wish to prove that every number not equal to one has a prime
factor:
!n. ~(n = 1) ==> ?p. prime p /\ p divides n
A natural way to prove this is by complete induction. Invoking
completeInduct_on `n` yields the goal
{ !m. m < n ==> ~(m = 1) ==> ?p. prime p /\ p divides m }
?-
~(n = 1) ==> ?p. prime p /\ p divides n