∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [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.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ}
  {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filterMapM f it) =
    Std.IterM.foldM
      (fun d b => do
        let __discr ← f b
        match __discr with
          | some c => pure (g d c)
          | x => pure d)
      init it