∀ {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] [LawfulMonad m] {s : Std.Slice γ} {init : δ}
  {f : δ → β → m δ}, List.foldlM f init s.toList = Std.Slice.foldlM f init s