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.