const CSNo : set prop const SNo_pair : set set set const CSNo_Re : set set const CSNo_Im : set set axiom CSNo_ReIm: !x:set.CSNo x -> x = SNo_pair (CSNo_Re x) (CSNo_Im x) claim !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Re x = CSNo_Re y -> CSNo_Im x = CSNo_Im y -> x = y