∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [Std.Iterator α₁ m β] [Std.Iterator α₂ m β] [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] [inst_4 : Monad m]
  [inst_5 : LawfulMonad m] [inst_6 : Std.IteratorLoop α₁ m m] [Std.LawfulIteratorLoop α₁ m m]
  [inst_8 : Std.IteratorLoop α₂ m m] [Std.LawfulIteratorLoop α₂ m m] {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → ita.drain = itb.drain