∀ {α : Type u_1} (head : α) (tail : List α),
  ∀ i < (head :: tail).length,
    ¬i + (List.drop i (List.take i (head :: tail))).length = 0 →
      i + (List.drop i (List.take i (head :: tail))).length - 1 < tail.length