∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  (it : Std.IterM m (β₁ × β₂)) (it₁' : Std.IterM m β₁) (out : β₁),
  it.internalState.left.IsPlausibleStep (Std.IterStep.yield it₁' out) → ∃ it, it.IsPlausibleOutput out