subst c1
α β : Type
inst✝ : DecidableEq α
f g : α → β
a : α
h1 : ∀ (x : α), ¬x = a → f x = g x
x : α
c1 : x = a
⊢ g a = g x
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : ∀ (x_1 : α), ¬x_1 = x → f x_1 = g x_1
⊢ g x = g x