∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Std.Do.WPMonad n ps] [inst_9 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_11 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← f b
          pure (g d c))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.mapM f it) ⦃Q⦄