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.CSNo x -> !p:set prop.(!y:set.!z:set.SNo y -> SNo z -> x = SNo_pair y z -> p (SNo_pair y z)) -> p x