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]
o : Option α
⊢ (Option.casesOn (id o) [] fun b => [b]) = o.toList
no goals