Theorem: Std.RBSet.isEmpty_iff_toList_eq_nil (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
t : RBSet α cmp
⊢ isEmpty t = true ↔ toList t = []
Tactic:
obtain ⟨⟨⟩, _⟩ := t <;> simp [toList, isEmpty]
State after:
no goals