∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f : (a : α) → β a → Option (γ a)) (size : ℕ) (k' : α)
  (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.filterMap! f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match f k' v' with
    | none => (Std.DTreeMap.Internal.Impl.filterMap! f l').link2! (Std.DTreeMap.Internal.Impl.filterMap! f r')
    | some v' =>
      Std.DTreeMap.Internal.Impl.link! k' v' (Std.DTreeMap.Internal.Impl.filterMap! f l')
        (Std.DTreeMap.Internal.Impl.filterMap! f r')