∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit},
  m.WF →
    ∀ {l : List α} {k : α},
      Std.DHashMap.Raw.Const.insertManyIfNewUnit m (k :: l) =
        Std.DHashMap.Raw.Const.insertManyIfNewUnit (m.insertIfNew k ()) l