∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [inst_3 : Std.IteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Std.Iter β},
  Std.Iter.foldM f init it = forIn it init fun x acc => ForInStep.yield <$> f acc x