const SNo_pair : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const CSNo_Re : set set const CSNo_Im : set set term add_CSNo = \x:set.\y:set.SNo_pair (CSNo_Re x + CSNo_Re y) (CSNo_Im x + CSNo_Im y) const CSNo : set prop const SNo : set prop axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) axiom CSNo_ReIm: !x:set.CSNo x -> x = SNo_pair (CSNo_Re x) (CSNo_Im x) const Empty : set axiom add_SNo_0L: !x:set.SNo x -> Empty + x = x axiom Im_0: CSNo_Im Empty = Empty axiom Re_0: CSNo_Re Empty = Empty claim !x:set.CSNo x -> add_CSNo Empty x = x