∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool} {k fallback : α},
  t.WF → (Std.TreeSet.Raw.filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback