∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Raw.filterMap (fun k => Option.guard fun v => f k v) t).Equiv (Std.DTreeMap.Raw.filter f t)