∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun k x => f k) t ⋯).impl.getKeyD k fallback =
    (Option.filter f (t.getKey? k)).getD fallback