const SNo : set prop const SNo_pair : set set set const Subq : set set prop axiom SNo_pair_prop_2_Subq: !x:set.!y:set.!z:set.!w:set.SNo y -> SNo z -> SNo w -> SNo_pair x y = SNo_pair z w -> Subq y w axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !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