∀ {α : Type u_1} (l : List α) (L : List (List α)),
  ∀ i < l.length,
    ∀ (_x_1 : 0 < (List.map List.length L).partialSums.length),
      ((fun x => decide (i < x)) ∘ fun x => l.length + x) (List.map List.length L).partialSums[0] = true ∧
        ∀ (j : ℕ) (hji : j < 0),
          ((fun x => decide (i < x)) ∘ fun x => l.length + x) (List.map List.length L).partialSums[j] = false