∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsStrictCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.gt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.gt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        l.toListModel ++ ⟨k', v'⟩ :: List.filter (fun x => k x.fst == Ordering.gt) r.toListModel