const SNo : set prop const SNo_pair : set set set term CSNo = \x:set.?y:set.SNo y & ?z:set.SNo z & x = SNo_pair y z claim !x:set.!y:set.SNo x -> SNo y -> ?z:set.SNo z & ?w:set.SNo w & SNo_pair x y = SNo_pair z w