∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k : α},
      Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l) k =
        if k ∈ m ∨ l.contains k = true then some () else none