∀ {α : Type u_1} (x : List α) (x_1 : ℕ) (x_2 : List α),
  List.MergeSort.Internal.splitRevAt.go✝ x x_1 x_2 =
    match x, x_1, x_2 with
    | x :: xs, n.succ, acc => List.MergeSort.Internal.splitRevAt.go✝¹ xs n (x :: acc)
    | xs, x, acc => (acc, xs)