const nat_p : set prop const SNo : set prop axiom nat_p_SNo: !x:set.nat_p x -> SNo x const exp_SNo_nat : set set set lemma !x:set.nat_p x -> SNo x -> !y:set.nat_p y -> nat_p (exp_SNo_nat x y) claim !x:set.nat_p x -> !y:set.nat_p y -> nat_p (exp_SNo_nat x y)