const nat_p : set prop const Empty : set axiom nat_0: nat_p Empty const mul_nat : set set set axiom mul_nat_0R: !x:set.mul_nat x Empty = Empty const add_nat : set set set axiom add_nat_p: !x:set.nat_p x -> !y:set.nat_p y -> nat_p (add_nat x y) const ordsucc : set set axiom mul_nat_SR: !x:set.!y:set.nat_p y -> mul_nat x (ordsucc y) = add_nat x (mul_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 (mul_nat x y)