const Empty : set const nat_p : set prop const ordsucc : set set axiom nat_inv_impred: !p:set prop.p Empty -> (!x:set.nat_p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x claim !x:set.nat_p x -> x = Empty | ?y:set.nat_p y & x = ordsucc y