∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  {motive : (Std.DHashMap.Raw α fun x => Unit) → Prop} (m : Std.DHashMap.Raw α fun x => Unit) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Raw α fun x => Unit) (a : α), motive m → motive (m.insertIfNew a ())) →
      motive (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l)