Theorem: isEmpty_toList (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
inst✝ : ToList C α
c : C
⊢ (toList c).isEmpty = isEmpty c
Tactic:
rw [isEmpty_eq_decide_size, List.isEmpty_eq_decide_length, size_eq_length_toList]
State after:
no goals