const SNo : set prop const ordsucc : set set const Empty : set axiom SNo_2: SNo (ordsucc (ordsucc Empty)) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLt_0_1: Empty < ordsucc Empty const exp_SNo_nat : set set set axiom exp_SNo_nat_0: !x:set.SNo x -> exp_SNo_nat x Empty = ordsucc Empty const nat_p : set prop axiom nat_p_SNo: !x:set.nat_p x -> SNo x axiom nat_ind: !p:set prop.p Empty -> (!x:set.nat_p x -> p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x lemma !x:set.nat_p x -> x < exp_SNo_nat (ordsucc (ordsucc Empty)) x -> SNo x -> ordsucc x < exp_SNo_nat (ordsucc (ordsucc Empty)) (ordsucc x) claim !x:set.nat_p x -> x < exp_SNo_nat (ordsucc (ordsucc Empty)) x