∀ {α : Type u_1} (a : List ℕ) (a_1 : List α) (a_2 : Array (List α)),
  List.takeListTR.go a a_1 a_2 =
    match a, a_1, a_2 with
    | [], xs, acc => (acc.toList, xs)
    | n :: ns, xs, acc =>
      match List.splitAt n xs with
      | (xs₁, xs₂) => List.takeListTR.go ns xs₂ (acc.push xs₁)