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
τ : 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
hm : Primrec fun p => p.2.2.depth
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
τ : 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
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2