theorem Std.Iterators.Iter.Equiv.toListRev_eq {α₁ β α₂ : Type u_1} [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] {ita : Iter β} {itb : Iter β} (h : ita.Equiv itb) : ita.toListRev = itb.toListRev

theorem Std.Iterators.Iter.Equiv.toList_eq {α₁ β α₂ : Type u_1} [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] {ita : Iter β} {itb : Iter β} (h : ita.Equiv itb) : ita.toList = itb.toList

theorem Std.Iterators.Iter.Equiv.toArray_eq {α₁ β α₂ : Type u_1} [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] {ita : Iter β} {itb : Iter β} (h : ita.Equiv itb) : ita.toArray = itb.toArray