∀ {α : Type u} (p : α → Bool) (x : List α) (x_1 : List α × List α),
  List.partition.loop p x x_1 =
    match x, x_1 with
    | [], (bs, cs) => (bs.reverse, cs.reverse)
    | a :: as, (bs, cs) =>
      match p a with
      | true => List.partition.loop p as (a :: bs, cs)
      | false => List.partition.loop p as (bs, a :: cs)