have : Primrec₂ (fun f t => funcL ⟨2, f⟩ [t.1, t.2] : L.Func 2 → Semiterm L μ n × Semiterm L μ n → Option (Semiterm L μ n)) :=
  (funcL_primrec' 2).comp₂ Primrec₂.left
    <| list_cons.comp₂ (fst.comp₂ Primrec₂.right) <| list_cons.comp₂ (snd.comp₂ Primrec₂.right) (Primrec₂.const [])
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])
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 ⟨2, f⟩ [t.1, t.2]
⊢ Primrec₂ fun a b => some (func a ![b.1, b.2])