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)
a : L.Func k
v : Fin k → UTerm L μ
⊢ WType.mk ((fun f => Sum.inr (Sum.inr ⟨k, f⟩)) a) ((fintypeArrowEquivFinArrow' ⋯).symm fun i => (equivW L μ) (v i)) =
    (equivW L μ) (func a v)
no goals