simp[funcL, Matrix.constant_eq_singleton]
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primrec₂ fun f t => funcL ⟨1, f⟩ [t]
f : L.Func 1
t : Semiterm L μ n
⊢ funcL ⟨1, f⟩ [t] = some (func f ![t])
no goals