Theorem: List.getCons?_eq_none (LeanColls/Data/List.lean)

State before:
α : Type u_1
c : List α
⊢ c.getCons? = none ↔ c = []
Tactic:
cases c <;> simp [getCons?]
State after:
no goals