∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_rcc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice t lowerBound...=upperBound) =
    List.filter (fun e => decide ((cmp e lowerBound).isGE = true ∧ (cmp e upperBound).isLE = true)) t.toList