∀ {α : Type u_1} (x : List ℕ) (x_1 : List α),
  x.splitLengths x_1 =
    match x, x_1 with
    | [], x => []
    | n :: ns, x =>
      match List.splitAt n x with
      | (x0, x1) => x0 :: ns.splitLengths x1