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