∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}},
  Std.HashMap.forM (fun a x => f a) m = Array.forM f m.keysArray