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

State before:
C : Type u_1
α : Type u_2
inst✝¹ : ToList C α
inst✝ : EmptyCollection C
inst : LawfulEmptyCollection C α
⊢ toList ∅ = []
Tactic:
rwa [ToList.lawfulEmptyCollection_iff] at inst
State after:
no goals