∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Finite α₂ m] {right : Std.IterM m β₂}
  {b' b : Option { out // ∃ it, it.IsPlausibleOutput out }} {left' left : Std.IterM m β₁},
  Option.SomeLtNone.lt emptyRelation b' b →
    Std.Iterators.Types.Zip.Rel₂ m { internalState := { left := left, memoizedLeft := b', right := right } }
      { internalState := { left := left', memoizedLeft := b, right := right } }