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