∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : (a : α) → β a → m PUnit.{w + 1}},
  Std.DTreeMap.Internal.Impl.forM f t = t.toListModel.forM fun a => f a.fst a.snd