case _ c1 =>
  subst c1
  contradiction
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
a : α
b : β
S_a : α
S_S : Finset α
a✝ : S_a ∉ S_S
S_ih : a ∉ S_S → Finset.image (updateITE f a b) S_S = Finset.image f S_S
h1_left : a ≠ S_a
h1_right : a ∉ S_S
c1 : S_a = a
⊢ b = f S_a
no goals