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