∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β}
  (h : l.Balanced), l.Ordered → (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v l h).2.impl.Ordered