∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  (f : (a : α) → a ∈ l → β → β) (init : β),
  (forIn' l init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (List.foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init l.attach)