claim !x:set.!y:set.!z:set.x = y -> y = z -> x = z