const nat_primrec : set (set set set) set set const Empty : set const add_nat : set set set term mul_nat = \x:set.nat_primrec Empty \y:set.add_nat x const nat_p : set prop const ordsucc : set set axiom nat_primrec_S: !x:set.!g:set set set.!y:set.nat_p y -> nat_primrec x g (ordsucc y) = g y (nat_primrec x g y) claim !x:set.!y:set.nat_p y -> mul_nat x (ordsucc y) = add_nat x (mul_nat x y)