∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{w + 1}}, Std.DHashMap.Raw.forM (fun a x => f a) ↑m = Array.forM f (↑m).keysArray