intro ⟨k, f⟩ l
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
⊢ ∀ (a : (k : ℕ) × L.Func k) (b : List (Semiterm L μ n)),
    encode (UTerm.funcL a (List.map (fun x => ↑(subtEquiv x)) b)) = encode (funcL a b)
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this✝ : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
⊢ encode (UTerm.funcL ⟨k, f⟩ (List.map (fun x => ↑(subtEquiv x)) l)) = encode (funcL ⟨k, f⟩ l)