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 SNo : set prop axiom SNo_Re: !x:set.SNo x -> CSNo_Re x = x const Empty : set axiom SNo_pair_0: !x:set.SNo_pair x Empty = x axiom SNo_0: SNo Empty axiom add_SNo_0L: !x:set.SNo x -> Empty + x = x axiom SNo_Im: !x:set.SNo x -> CSNo_Im x = Empty claim !x:set.!y:set.SNo x -> SNo y -> x + y = add_CSNo x y