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 ordsuccI1: !x:set.Subq x (ordsucc x) const nat_p : set prop const If_i : prop set set set lemma !x:set.!f:set set.!y:set.!z:set.!w:set.nat_p x -> (!u:set.u iIn ordsucc (ordsucc x) -> !v:set.v iIn ordsucc (ordsucc x) -> f u = f v -> u = v) -> w iIn ordsucc x -> z iIn ordsucc (ordsucc x) -> ordsucc z iIn ordsucc (ordsucc x) -> 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 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 z iIn ordsucc x hyp w iIn ordsucc x hyp z iIn ordsucc (ordsucc x) claim ordsucc z 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