\doc{Sample proofs: an alternate induction rule}

In order to prove a final theorem about subsets, \fq{x \subseteq x}, it helps
to use a different induction principle than the one we asserted as an axiom.
We can prove that \plink{of-ir}{induction rule} as follows:
\begin{verbatim}
prove sort S generated by {}, {__}, \union
    resume by induction
      set name lemma
      critical-pairs *GenHyp with *GenHyp
      critical-pairs *InductHyp with lemma
qed
\end{verbatim}
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
\fq{isGenerated}:
\begin{verbatim}
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)
\end{verbatim}
The user then directs LP to attempt to prove \fq{isGenerated(s)} by induction
(on \fq{s}) using the asserted induction rule.  LP proves the basis subgoal 
automatically using the hypothesis \fq#isGenerated({})#.  The user guides the
proof of the induction subgoal by causing LP to compute critical pairs.  The
first \clink{critical-pairs} command causes LP to derive
\begin{verbatim}
lemma.1: isGenerated(s) => isGenerated(insert(e, s))
\end{verbatim}
as a critical pair between the second and third \fq{isGenerated} hypotheses.
The second \clink{critical-pairs} command causes LP to derive the induction
subgoal, \fq{isGenerated(insert(e, sc))}, as a critical pair between this lemma
and the induction hypothesis.  This finishes the proof of the induction rule.