∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {motive : Std.ExtDHashMap α β → Prop} (m : Std.ExtDHashMap α β)
  (l : ρ),
  motive m → (∀ (m : Std.ExtDHashMap α β) (a : α) (b : β a), motive m → motive (m.insert a b)) → motive (m.insertMany l)