subst a1
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
a : α
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
a1 : x = a
⊢ f x = f a
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
g : β → γ
b : γ
h1 : ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
x : α
⊢ f x = f x