∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_7 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β} {f : β → n β₂} {init : γ}
  {g : β₂ → γ → o (ForInStep γ)},
  forIn (Std.Iter.mapM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      g __do_lift acc