{m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [inst_2 : Monad m] →
            [Std.Iterators.Finite α₁ m] →
              [Std.Iterators.Productive α₂ m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Zip α₁ m α₂ β₂) m