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 nat_p : set prop const ordsucc : set set axiom nat_ordsucc: !x:set.nat_p x -> nat_p (ordsucc x) axiom nat_ordsucc_in_ordsucc: !x:set.nat_p x -> !y:set.y iIn x -> ordsucc y iIn ordsucc x 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) -> z iIn ordsucc x -> w iIn ordsucc x -> z iIn ordsucc (ordsucc x) -> 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 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 claim 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