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_2: !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> SNo w -> SNo_pair x y = SNo_pair z w -> y = w const CSNo_Re : set set axiom CSNo_Re2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Re (SNo_pair x y) = x const CSNo_Im : set set axiom CSNo_Im1: !x:set.CSNo x -> SNo (CSNo_Im x) & x = SNo_pair (CSNo_Re x) (CSNo_Im x) claim !x:set.!y:set.SNo x -> SNo y -> CSNo_Im (SNo_pair x y) = y