const In : set set prop term iIn = In infix iIn 2000 2000 term bij = \x:set.\y:set.\f:set set.(!z:set.z iIn x -> f z iIn y) & (!z:set.z iIn x -> !w:set.w iIn x -> f z = f w -> z = w) & !z:set.z iIn y -> ?w:set.w iIn x & f w = z const If_i : prop set set set axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x const ordsucc : set set axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom xm: !P:prop.P | ~ P const nat_p : set prop axiom PigeonHole_nat: !x:set.nat_p x -> !f:set set.(!y:set.y iIn ordsucc x -> f y iIn x) -> ~ !y:set.y iIn ordsucc x -> !z:set.z iIn ordsucc x -> f y = f z -> y = z axiom dneg: !P:prop.~ ~ P -> P lemma !x:set.!f:set set.!y:set.!z:set.!w:set.(!u:set.u iIn x -> !v:set.v iIn x -> f u = f v -> u = v) -> ~ (?u:set.u iIn x & f u = y) -> z iIn ordsucc x -> w iIn ordsucc x -> (z != x -> z iIn x) -> If_i (z = x) y (f z) = If_i (w = x) y (f w) -> z = w claim !x:set.nat_p x -> !f:set set.(!y:set.y iIn x -> f y iIn x) -> (!y:set.y iIn x -> !z:set.z iIn x -> f y = f z -> y = z) -> (!y:set.y iIn x -> f y iIn x) & (!y:set.y iIn x -> !z:set.z iIn x -> f y = f z -> y = z) & !y:set.y iIn x -> ?z:set.z iIn x & f z = y