∀ {α β : 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 : (out : β) → out ∈ it → γ → m (ForInStep γ)},
  forIn' it init f =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let __do_lift ← f out ⋯ init
      match __do_lift with
        | ForInStep.yield c => forIn' it' c fun out_1 h'' acc => f out_1 ⋯ acc
        | ForInStep.done c => pure c
    | ⟨Std.IterStep.skip it', h⟩ => forIn' it' init fun out h' acc => f out ⋯ acc
    | ⟨Std.IterStep.done, property⟩ => pure init