exact (option_casesOn Primrec.id (const []) (this.comp₂ Primrec₂.right)).of_eq
  (fun o => by rcases o <;> simp)
α : 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
no goals