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