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 nat_ordsucc: !x:set.nat_p x -> nat_p (ordsucc x) lemma !p:set prop.(!x:set.nat_p x -> p x -> p (ordsucc x)) -> nat_p Empty & p Empty -> (!x:set.nat_p x & p x -> nat_p (ordsucc x) & p (ordsucc x)) -> !x:set.nat_p x -> p x var p:set prop hyp p Empty hyp !x:set.nat_p x -> p x -> p (ordsucc x) claim nat_p Empty & p Empty -> !x:set.nat_p x -> p x