∀ {γ : Type u} {α β : Type v} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [Std.Iterators.Finite α Id] [inst_3 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  [inst_5 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ], s.iter.length = s.size