const nat_p : set prop const Empty : set axiom nat_0: nat_p Empty const ordsucc : set set axiom nat_ordsucc: !x:set.nat_p x -> nat_p (ordsucc x) claim nat_p (ordsucc Empty)