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 Empty : set const ordsucc : set set term nat_p = \x:set.!p:set prop.p Empty -> (!y:set.p y -> p (ordsucc y)) -> p x axiom EmptyE: !x:set.nIn x Empty axiom FalseE: ~ False axiom ordsuccI2: !x:set.x iIn ordsucc x axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x lemma !x:set.!y:set.(!z:set.z iIn x -> ordsucc z iIn ordsucc x) -> y iIn x -> ordsucc y iIn ordsucc x -> ordsucc y iIn ordsucc (ordsucc x) claim !x:set.nat_p x -> !y:set.y iIn x -> ordsucc y iIn ordsucc x