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