simp[funcL]
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
x✝ : σ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₂
⊢ funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x✝ k f v)
no goals