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) var x:set var f:set set var y:set var z:set var w:set hyp !u:set.u iIn ordsucc (ordsucc x) -> !v:set.v iIn ordsucc (ordsucc x) -> f u = f v -> u = v hyp ordsucc z iIn ordsucc (ordsucc x) hyp w iIn ordsucc (ordsucc x) hyp Subq y z hyp ~ Subq y w hyp f (ordsucc z) = f w claim ordsucc z != w