∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.DHashMap α fun x => Unit}
  (l : List α),
  m₁.Equiv m₂ → (Std.DHashMap.Const.insertManyIfNewUnit m₁ l).Equiv (Std.DHashMap.Const.insertManyIfNewUnit m₂ l)