subst h1
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
h1 : f x = x'
⊢ image f S \ {x'} = image f (S \ {x}) \ {x'}
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
⊢ image f S \ {f x} = image f (S \ {x}) \ {f x}