simp only [Function.updateITE]
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ updateITE f y z x = f x
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ (if x = y then z else f x) = f x