∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β}
  {f : γ → β → m γ} {init : γ}, List.foldlM f init it.toList.run = Std.IterM.foldM f init it