intro a a1
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
⊢ ∀ ⦃x_1 : α⦄, x_1 ∈ ↑(S \ {x}) → Function.updateITE f x x' x_1 = f x_1
case h
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
x' : β
f : α → β
a : α
a1 : a ∈ ↑(S \ {x})
⊢ Function.updateITE f x x' a = f a