const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoLe_ref: !x:set.x <= x const SNo : set prop const exp_SNo_nat : set set set const Empty : set const ordsucc : set set axiom exp_SNo_nat_0: !x:set.SNo x -> exp_SNo_nat x Empty = ordsucc Empty const nat_p : set prop axiom SNo_exp_SNo_nat: !x:set.SNo x -> !y:set.nat_p y -> SNo (exp_SNo_nat x y) 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.!y:set.SNo x -> ordsucc Empty <= x -> nat_p y -> ordsucc Empty <= exp_SNo_nat x y -> SNo (exp_SNo_nat x y) -> ordsucc Empty <= exp_SNo_nat x (ordsucc y) claim !x:set.SNo x -> ordsucc Empty <= x -> !y:set.nat_p y -> ordsucc Empty <= exp_SNo_nat x y