∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : δ → (a : α) → β a → m δ} {init : δ} {b : Std.DHashMap.Raw α β},
  Std.DHashMap.Raw.Internal.foldRevM f init b =
    List.foldrM (fun a b => f b a.fst a.snd) init (Std.DHashMap.Internal.toListModel b.buckets)