simp only [Function.updateITE]
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ updateITE f a b x = Function.updateITE' f a b x
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
x : α
⊢ (if x = a then b else f x) = Function.updateITE' f a b x