∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m PUnit.{w + 1}},
  Std.DTreeMap.Raw.forM f t = Std.DTreeMap.Raw.Const.forMUncurried (fun a => f a.1 a.2) t