∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type u_1}
  [inst_1 : Std.Iterator α₂ m β₂] [inst_2 : Std.Iterators.Finite α₁ m] [inst_3 : Std.Iterators.Productive α₂ m],
  WellFounded (Std.Iterators.Types.Zip.Rel₁ m)