∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1}
  {o : Type w → Type u_2} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o]
  [inst_5 : Std.Do.WPMonad o ps] [inst_6 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_9 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filterMapWithPostcondition f it) init g ⦃Q⦄