const nat_p : set prop const Empty : set axiom nat_0: nat_p Empty const add_nat : set set set axiom add_nat_0R: !x:set.add_nat x Empty = x const ordsucc : set set axiom add_nat_SR: !x:set.!y:set.nat_p y -> add_nat x (ordsucc y) = ordsucc (add_nat x y) claim add_nat (ordsucc Empty) (ordsucc Empty) = ordsucc (ordsucc Empty)