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 p l => List.map f l
no goals