const nat_primrec : set (set set set) set set const ordsucc : set set const Empty : set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 term exp_SNo_nat = \x:set.nat_primrec (ordsucc Empty) \y:set.mul_SNo x const nat_p : set prop 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) const SNo : set prop claim !x:set.SNo x -> !y:set.nat_p y -> exp_SNo_nat x (ordsucc y) = x * exp_SNo_nat x y