∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (init : β),
  forIn' xs init f =
    ForInStep.value <$>
      Vector.foldlM
        (fun b x =>
          match x with
          | ⟨a, m_1⟩ =>
            match b with
            | ForInStep.yield b => f a m_1 b
            | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) xs.attach