simp
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ (if x = a then a else if x = b then c else id x) = if x = b then c else id x
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
⊢ x = a → a = if x = b then c else x