# LP, the Larch Prover -- Sample proofs: an alternate induction rule

In order to prove a final theorem about subsets, x \subseteq x, it helps to use a different induction principle than the one we asserted as an axiom. We can prove that induction rule as follows:
```prove sort S generated by {}, {__}, \union
resume by induction
set name lemma
critical-pairs *GenHyp with *GenHyp
critical-pairs *InductHyp with lemma
qed
```
LP formulates an appropriate subgoal for the proof of this conjecture, together with additional hypotheses to be used in the proof, using a new operator isGenerated:
```Creating subgoals for proof of induction rule
Induction subgoal hypotheses:
setTheoremsGenHyp.1: isGenerated({})
setTheoremsGenHyp.2: isGenerated({e})
setTheoremsGenHyp.3:
isGenerated(s) /\ isGenerated(s1) => isGenerated(s \union s1)
Induction subgoal:
isGenerated(s)
```
The user then directs LP to attempt to prove isGenerated(s) by induction (on s) using the asserted induction rule. LP proves the basis subgoal automatically using the hypothesis isGenerated({}). The user guides the proof of the induction subgoal by causing LP to compute critical pairs. The first critical-pairs command causes LP to derive
```lemma.1: isGenerated(s) => isGenerated(insert(e, s))
```
as a critical pair between the second and third isGenerated hypotheses. The second critical-pairs command causes LP to derive the induction subgoal, isGenerated(insert(e, sc)), as a critical pair between this lemma and the induction hypothesis. This finishes the proof of the induction rule.