The command

The command `resume by induction` directs LP to resume the proof of the
current conjecture by induction.

LP supports proofs both by structural and well-founded induction. Induction
rules beginning with `generated by` provide the basis for proofs by
structural induction. Induction rules beginning with
`well founded` provide the basis for proofs by
well-founded induction.

LP generates appropriate subgoals for each kind of proof by induction. Some of
those subgoals introduce additional hypotheses, known as
*induction hypotheses*.
The names of the induction hypotheses have the form
<simpleId>`InductHyp.`<number>, where <simpleId> is the current value
of the name-prefix setting.