have : Primrec₂ (fun z (p : σ × WType β) => WType.elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) p.1 p.2) :=
  to₂' <| by {
    have hm : Primrec (fun (p : τ × σ × WType β) => p.2.2.depth) := w_depth.comp <| snd.comp snd
    have hl : Primrec (fun (p : τ × σ × WType β) =>
        p.2.2.inversion.2.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w))) :=
      list_map (snd.comp $ w_inversion.comp $ snd.comp snd)
        <| Primrec₂.pair.comp (fst.comp fst)
        <| Primrec₂.pair.comp
          (hfs.comp (fst.comp fst)
            (Primrec₂.pair.comp
              (fst.comp $ w_inversion.comp $ snd.comp $ snd.comp fst)
              (fst.comp $ snd.comp fst)))
        <| snd
    have hg : Primrec₂ (fun (p : τ × σ × WType β) (l : List γ) => fγ p.1 (p.2.1, p.2.2.inversion.1, l)) :=
      hfγ.comp₂ (fst.comp₂ Primrec₂.left)
        <| Primrec₂.pair.comp₂ (fst.comp₂ $ snd.comp₂ Primrec₂.left)
        <| Primrec₂.pair.comp₂ (fst.comp₂ $ w_inversion.comp₂ $ snd.comp₂ $ snd.comp₂ Primrec₂.left) Primrec₂.right
    apply nat_omega_rec' _ hm hl (option_some.comp₂ hg)
      (by rintro ⟨z, x, ⟨a, f⟩⟩ ⟨z', x', w'⟩
          simp[inversion, Function.comp, List.mem_ofFn]
          rintro rfl rfl i rfl; exact depth_lt_depth_mk _ _ _)
      (by { rintro ⟨z, x, ⟨a, f⟩⟩; simp[inversion, Function.comp, elimvL_mk]
            congr }) }
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
⊢ Primrec fun z => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (g z) (w z)
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
this : Primrec₂ fun z p => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) p.1 p.2
⊢ Primrec fun z => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (g z) (w z)