∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ] {f : β → m (Std.IterM m γ)}
  {it₁ it₁' : Std.Iter β} {it₂' : Std.IterM m γ} {b : β},
  it₁.IsPlausibleStep (Std.IterStep.yield it₁' b) →
    MonadAttach.CanReturn (f b) it₂' →
      (Std.Iter.flatMapAfterM f it₁ none).IsPlausibleStep
        (Std.IterStep.skip (Std.Iter.flatMapAfterM f it₁' (some it₂')))