∀ {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn f init t =
    forIn (Std.DTreeMap.Internal.Impl.Const.toList t) init fun a b => f a.1 a.2 b