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

theorem Std.Slice.Internal.forIn_iter {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] {δ : Type w} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn (iter s) init f = forIn s init f

theorem Std.Slice.Internal.size_eq_length_iter {γ : Type u} {α β : Type v} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] : s.size = (iter s).length

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

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

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

theorem Std.Slice.Internal.fold_iter {γ : Type u} {α β : Type v} {α✝ : Type u_1} {f : α✝ → β → α✝} {init : α✝} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {s : Slice γ} : Iter.fold f init (iter s) = foldl f init s

theorem Std.Slice.Internal.foldM_iter {γ : Type u} {α β : Type v} {δ : Type w} {init : δ} {m : Type w → Type w'} [Monad m] [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] [Iterators.Finite α Id] {s : Slice γ} {f : δ → β → m δ} : Iter.foldM f init (iter s) = foldlM f init s