have h₁ := w_mkFin (β := Edge L μ)
  (fun f => (Sum.inr $ Sum.inr ⟨k, f⟩) : L.Func k → Node L μ)
  (fun _ => Fintype.card_fin k)
  (sum_inr.comp $ sum_inr.comp $ sigma_pair k)
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
⊢ 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)
⊢ Primrec₂ fun a b => (equivW L μ) (func a b)