assert sort Nat generated by 0, s prove 0 + x = x by induction Basis subgoal: 0 + 0 = 0 New constant: xc Induction hypothesis: 0 + xc = xc Induction subgoal: 0 + s(xc) = s(xc)
assert sort Set generated by {}, {__}, \U prove x \subseteq x by induction Basis subgoals: {} \subseteq {}, {e} \subseteq {e} New constants: xc, xc1 Induction hypotheses: xc \subseteq xc, xc1 \subseteq xc1 Induction subgoal: (xc \U xc1) \subseteq (xc \U xc1)