∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.filter! f (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    match f k' v' with
    | false => (Std.DTreeMap.Internal.Impl.filter! f l').link2! (Std.DTreeMap.Internal.Impl.filter! f r')
    | true =>
      Std.DTreeMap.Internal.Impl.link! k' v' (Std.DTreeMap.Internal.Impl.filter! f l')
        (Std.DTreeMap.Internal.Impl.filter! f r')