const UPair : set set set term Sing = \x:set.UPair x x const In : set set prop term iIn = In infix iIn 2000 2000 axiom UPairE: !x:set.!y:set.!z:set.x iIn UPair y z -> x = y | x = z claim !x:set.!y:set.y iIn Sing x -> y = x