∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {km : α}, t.min! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true