theorem Std.Slice.Internal.iter_eq_iter {γ : Type u} {β : Type v} {s : Slice γ} [Iterators.ToIterator s Id β] : s.iter = iter s

theorem Std.Slice.iter_eq_toIteratorIter {β : Type v} {γ : Type u} {s : Slice γ} [Iterators.ToIterator s Id β] : s.iter = Iterators.ToIterator.iter s

theorem Std.Slice.size_eq_size_iter {γ : Type u} {β : Type v} {s : Slice γ} [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorSize (Iterators.ToIterator.State s Id) Id] : s.size = s.iter.size

theorem Std.Slice.toArray_eq_toArray_iter {γ : Type u} {β : Type v} {s : Slice γ} [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] : s.toArray = s.iter.toArray

theorem Std.Slice.toList_eq_toList_iter {γ : Type u} {β : Type v} {s : Slice γ} [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] : s.toList = s.iter.toList

theorem Std.Slice.toListRev_eq_toListRev_iter {γ : Type u} {β : Type v} {s : Slice γ} [Iterators.ToIterator s Id β] [Iterators.Iterator (Iterators.ToIterator.State s Id) Id β] [Iterators.Finite (Iterators.ToIterator.State s Id) Id] : s.toListRev = s.iter.toListRev