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