∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k : α},
  Std.DTreeMap.Internal.Impl.contains k
      ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯) =
    (List.map Prod.fst l).contains k