∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ it₂' : Std.IterM m γ} {b : γ},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' b) →
    (Std.IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep
      (Std.IterStep.yield (Std.IterM.flatMapAfter f it₁ (some it₂')) b)