∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α)
  (f : (a : α) → a ∈ as → β → m (ForInStep β)) (x : List α) (x_1 : β) (x_2 : ∃ bs, bs ++ x = as),
  List.forIn'.loop as f x x_1 x_2 =
    match x, x_1, x_2 with
    | [], b, x => pure b
    | a :: as', b, h =>
      have this := ⋯;
      do
      let __do_lift ← f a this b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          have this := ⋯;
          List.forIn'.loop as f as' b this