∀ {α : Type u} {β : Type v} {ρ : Type w} [inst : ForIn Id ρ (α × β)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertMany m l =
    (have r := ⟨m, ⋯⟩;
      do
      let r ←
        forIn l r fun x r =>
            let r_1 := r;
            match x with
            | (a, b) =>
              have r := ⟨(↑r_1).insert a b, ⋯⟩;
              do
              pure PUnit.unit
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) →
              P m → P m' } :=
        r
      pure r).run