@[simp]

theorem Option.mem_toList {α : Type u_1} {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o