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 axiom nat_primrec_0: !x:set.!g:set set set.nat_primrec x g Empty = x claim !x:set.mul_nat x Empty = Empty