∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)}
  {g : γ → Std.Iterators.PostconditionT o (Option δ)} {fg : β → Std.Iterators.PostconditionT o (Option δ)}
  {it : Std.IterM m β},
  (∀ (b : β),
      (fg b).run = do
        let __do_lift ← liftM (f b).run
        match __do_lift with
          | none => pure none
          | some fb => (g fb).run) →
    (Std.IterM.filterMapWithPostcondition g (Std.IterM.filterMapWithPostcondition f it)).toList =
      (Std.IterM.filterMapWithPostcondition fg it).toList