have : Primrec (fun a => [a] : α → List α) := list_cons.comp Primrec.id (const [])
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
⊢ Primrec Option.toList
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
this : Primrec fun a => [a]
⊢ Primrec Option.toList