∀ {α : Type u_1} (x : List α) (x_1 : List ℕ),
  x.splitWrtCompositionAux x_1 =
    match x, x_1 with
    | x, [] => []
    | l, n :: ns =>
      match List.splitAt n l with
      | (l₁, l₂) => l₁ :: l₂.splitWrtCompositionAux ns