subst a1
case h
α : Type
inst✝ : DecidableEq α
a b c : α
h1 : ¬a = b
x : α
a1 : x = a
⊢ a = if x = b then c else x
case h
α : Type
inst✝ : DecidableEq α
b c x : α
h1 : ¬x = b
⊢ x = if x = b then c else x