∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (countdown : ℕ) (inner : Std.IterM m β)
  (finite : countdown > 0 ∨ Std.Iterators.Finite α m) (countdown_1 : ℕ) (inner_1 : Std.IterM m β)
  (finite_1 : countdown_1 > 0 ∨ Std.Iterators.Finite α m),
  ({ countdown := countdown, inner := inner, finite := finite } =
      { countdown := countdown_1, inner := inner_1, finite := finite_1 }) =
    (countdown = countdown_1 ∧ inner = inner_1)