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