intro a1
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
⊢ x = b → d = c
case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
b : α
c d : β
x : α
c2 h1 : ¬x = b
a1 : x = b
⊢ d = c