∀ {ps : Std.Do.PostShape} {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps] [inst_9 : Std.IteratorLoop α Id n]
  [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_13 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ}
  {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← liftM (f b)
          if __do_lift.down = true then g d b else pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.filterM f it) ⦃Q⦄