∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        ∀ {h' : k' ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l},
          k ∉ m →
            List.Pairwise (fun a b => (a == b) = false) l →
              k ∈ l → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey k' h' = k