const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term nIn = \x:set.\y:set.~ x iIn y const ordsucc : set set axiom ordsucc_inj: !x:set.!y:set.ordsucc x = ordsucc y -> x = y const If_i : prop set set set axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x axiom FalseE: ~ False axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom xm: !P:prop.P | ~ P lemma !x:set.!f:set set.!y:set.!z:set.!w:set.(!u:set.u iIn ordsucc (ordsucc x) -> !v:set.v iIn ordsucc (ordsucc x) -> f u = f v -> u = v) -> ordsucc z iIn ordsucc (ordsucc x) -> w iIn ordsucc (ordsucc x) -> Subq y z -> ~ Subq y w -> f (ordsucc z) = f w -> ordsucc z != w lemma !x:set.!f:set set.!y:set.!z:set.!w:set.(!u:set.u iIn ordsucc (ordsucc x) -> !v:set.v iIn ordsucc (ordsucc x) -> f u = f v -> u = v) -> z iIn ordsucc (ordsucc x) -> ordsucc w iIn ordsucc (ordsucc x) -> ~ Subq y z -> Subq y w -> f z = f (ordsucc w) -> z != ordsucc w const nat_p : set prop var x:set var f:set set var y:set var z:set var w:set hyp nat_p x hyp !u:set.u iIn ordsucc (ordsucc x) -> !v:set.v iIn ordsucc (ordsucc x) -> f u = f v -> u = v hyp w iIn ordsucc x hyp z iIn ordsucc (ordsucc x) hyp ordsucc z iIn ordsucc (ordsucc x) hyp w iIn ordsucc (ordsucc x) claim ordsucc w iIn ordsucc (ordsucc x) -> If_i (Subq y z) (f (ordsucc z)) (f z) = If_i (Subq y w) (f (ordsucc w)) (f w) -> z = w