exact Eq.symm <| h n (Nat.zero_le n)
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : ℕ → α
hf : Primrec f
g : ℕ → α
h : ∀ x ≥ 0, g x = f x
n : ℕ
⊢ f n = g n
no goals