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