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

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

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