have : Primrec (fun e => encode $ ((encodeDecode (Fin k → α) e).bind
  $ fun c => (decode c : Option (List α)).map (fun l => l.map f)) : ℕ → ℕ) :=
  (Primrec.encode.comp $ option_bind Primrec.encodeDecode
    (option_map (Primrec.decode.comp snd) (by apply list_map snd (hf.comp₂ Primrec₂.right))))
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
⊢ Primrec fun v i => f (v i)
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → σ
hf : Primrec f
k : ℕ
this :
  Primrec fun e => encode ((encodeDecode (Fin k → α) e).bind fun c => Option.map (fun l => List.map f l) (decode c))
⊢ Primrec fun v i => f (v i)