exact (Primrec₂.comp₂ h₁ Primrec₂.left (h₂.comp₂ Primrec₂.right)).of_eq
  (fun a v => by simp[equivW, toW, Edge])
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)
no goals