∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Min α] [inst_1 : LE α]
  [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [Std.LawfulEqCmp cmp],
  t.toList.head? = t.min?