const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const CSNo_Im : set set const SNo_pair : set set set axiom CSNo_Im2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Im (SNo_pair x y) = y axiom SNo_pair_0: !x:set.SNo_pair x Empty = x claim !x:set.SNo x -> CSNo_Im x = Empty