funext x
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
⊢ updateITE (updateITE f a d) b c = updateITE (updateITE f b c) a d
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a b : α
c d : β
h1 : ¬a = b
x : α
⊢ updateITE (updateITE f a d) b c x = updateITE (updateITE f b c) a d x