have : Primrec₂ (fun x w => Nat.pair (w.depth + 1) (Nat.pair (encode $ f x) (encode [(encode w).unpair.2])) : σ → WType β → ℕ) :=
  Primrec₂.natPair.comp
    (succ.comp $ w_depth.comp snd)
    (Primrec₂.natPair.comp (Primrec.encode.comp $ hf.comp fst)
      (Primrec.encode.comp $ list_cons.comp (snd.comp $ unpair.comp $ Primrec.encode.comp snd) (const [])))
τ : 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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
⊢ Primrec₂ fun x w => WType.mk (f x) fun x => w
τ : 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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
⊢ Primrec₂ fun x w => WType.mk (f x) fun x => w