have h₂ : Primrec (fun v => (fun i => equivW L μ (v i)) : (Fin k → UTerm L μ) → (Fin k → WType (Edge L μ))) :=
  finArrow_map Primrec.of_equiv k
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
h₁ : Primrec₂ fun x w => WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
h₂ : Primrec fun v i => (equivW L μ) (v i)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)