∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      compare k k' = Ordering.eq →
        ∀
          {h' :
            Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) = true},
          k ∉ t →
            List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
              k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey k' h' = k