Theorem: List.isEmpty_eq_decide_length (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
l : List α
⊢ l.isEmpty = decide (l.length = 0)
Tactic:
cases l <;> simp [isEmpty]
State after:
no goals