@user21820 Is the following correct? Prove that forall n in N forall m in N if m in n then m subset n.
1) Induct on n.
n = 0, true.
let n = n0, so we have forall m in N if m in n0 then m subset n0.
[Goal: forall m in N if m in S(n0) then m subset S(n0)]
2) induct on m
m = 0, if 0 in S(n0) then 0 subset S(n0), true.
let m = m0, so we have if m0 in S(n0) then m0 subset S(n0)
[New goal: if S(m0) in S(n0) then S(m0) subset S(n0)]
Suppose S(m0) in S(n0)
S(n0) = n0 cup {n0}
S(m0) in n0 or S(m0) in {n0}