const SNo : set prop const CSNo : set prop const SNo_pair : set set set axiom CSNo_I: !x:set.!y:set.SNo x -> SNo y -> CSNo (SNo_pair x y) axiom SNo_pair_prop_1: !x:set.!y:set.!z:set.!w:set.SNo x -> SNo z -> SNo_pair x y = SNo_pair z w -> x = z const CSNo_Re : set set axiom CSNo_Re1: !x:set.CSNo x -> SNo (CSNo_Re x) & ?y:set.SNo y & x = SNo_pair (CSNo_Re x) y claim !x:set.!y:set.SNo x -> SNo y -> CSNo_Re (SNo_pair x y) = x