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