∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : β → γ → m (ForInStep γ)}, forIn it.toList init f = forIn it init f