apply Finset.image_congr
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
a b : β
f : α → β
⊢ image (Function.updateITE f x a) (S \ {x}) = image (Function.updateITE f x b) (S \ {x})
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
a b : β
f : α → β
⊢ Set.EqOn (Function.updateITE f x a) (Function.updateITE f x b) ↑(S \ {x})