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