∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} {l : List α} {k : α},
  Std.DTreeMap.Raw.Const.insertManyIfNewUnit t (k :: l) =
    Std.DTreeMap.Raw.Const.insertManyIfNewUnit (t.insertIfNew k ()) l