have : Primrec₂ (fun x w => Nat.pred $ encode (WType.mkL (f x) (List.ofFn w)) : σ → (Fin k → WType β) → ℕ) :=
  (pred.comp $ Primrec.encode.comp $ w_mkL.comp (hf.comp fst) (finArrow_list_ofFn.comp 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 γ
f : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm 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 : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) (List.ofFn w))).pred
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm w)