Perform complete induction with a supplied measure function.
DESCRIPTION
If q parses into a well-typed term M N, an invocation
measureInduct_on q begins a proof by induction, using M to map
N into a number. The term N should occur free in the current goal.
FAILURE
If M N does not parse into a term or if N does not occur free in the
current goal.
EXAMPLE
Suppose we wish to prove P (APPEND l1 l2) by induction on the length of
l1. Then measureInduct_on `LENGTH ll` yields the goal
{ !y. LENGTH y < LENGTH l1 ==> P (APPEND y l2) } ?- P (APPEND l1 l2)