∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : List α)
  (f : (i : ℕ) → α → i < as.length → m β) (x : Array β) (x_1 : [].length + x.size = as.length),
  List.mapFinIdxM.go as f [] x x_1 = pure x.toList