have := (Primrec.of_equiv_symm (e := equivW L μ)).comp₂
  ((this.comp₂ (Primrec₂.const ()) Primrec.id.to₂).comp₂
    ((Primrec.of_equiv (e := equivW L μ)).comp₂ Primrec₂.left)
    ((Primrec.of_equiv (e := equivW L μ)).comp₂ Primrec₂.right))
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
⊢ Primrec₂ and
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ :
  Primrec₂ fun x w =>
    WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
this :
  Primrec₂ fun a b =>
    (equivW L μ).symm
      (WType.mk ((fun x => (true, Sum.inr (Sum.inr (Sum.inl ())))) ())
        ((fintypeArrowEquivFinArrow' ⋯).symm
          ![(id ((equivW L μ) a, (equivW L μ) b)).1, (id ((equivW L μ) a, (equivW L μ) b)).2]))
⊢ Primrec₂ and