The new induction rule,

The prove command directs LP to use the induction rule just proved to formulate subgoals for the proof by induction using the generatorsprove x \subseteq (x \union y) by induction on x using setTheorems qed

LP establishes all three subgoals automatically.Creating subgoals for proof by structural induction on `x' Basis subgoals: Subgoal 1: {} \subseteq ({} \union y) Subgoal 2: {e} \subseteq ({e} \union y) Induction constants: xc, xc1 Induction hypotheses: setTheoremsInductHyp.1: xc \subseteq (xc \union y) setTheoremsInductHyp.2: xc1 \subseteq (xc1 \union y) Induction subgoal: Subgoal 3: (xc \union xc1) \subseteq (xc1 \union xc \union y)

Finally, we prove the last theorem by directing LP to compute a critical pair
between the theorem just established and an earlier theorem,
`x \union {} = x`.

prove x \subseteq x critical-pairs setTheorems with setTheorems qed