theorem Std.Iterators.IterM.Equiv.toListRev_eq {m : Type u_1 → Type u_2} {α₁ β α₂ : Type u_1} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : ita.toListRev = itb.toListRev

theorem Std.Iterators.IterM.Equiv.toList_eq {β α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] [IteratorCollect α₁ m m] [LawfulIteratorCollect α₁ m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α₂ m m] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : ita.toList = itb.toList

theorem Std.Iterators.IterM.Equiv.toArray_eq {m : Type u_1 → Type u_2} {α₁ β α₂ : Type u_1} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] [IteratorCollect α₁ m m] [LawfulIteratorCollect α₁ m m] [IteratorCollect α₂ m m] [LawfulIteratorCollect α₂ m m] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : ita.toArray = itb.toArray