∀ {α : Type u} (R : α → α → Bool) (x : List α) (x_1 : α) (x_2 : List α) (x_3 : List (List α)),
  List.splitBy.loop R x x_1 x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | a :: as, b, r, acc =>
      match R b a with
      | true => List.splitBy.loop R as a (b :: r) acc
      | false => List.splitBy.loop R as a [] ((b :: r).reverse :: acc)
    | [], ag, r, acc => ((ag :: r).reverse :: acc).reverse