∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Internal.Raw₀ α β} {l : ρ},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑↑(m.insertMany l)