∀ {α : Type u_1} (motive : (x x_1 : ℕ) → (x_2 : List α) → x < x_2.length → x_1 ≤ x → Prop) (x x_1 : ℕ) (x_2 : List α)
  (x_3 : x < x_2.length) (x_4 : x_1 ≤ x),
  (∀ (x : ℕ) (head : α) (tail : List α) (x_5 : x < (head :: tail).length) (x_6 : 0 ≤ x),
      motive x 0 (head :: tail) x_5 x_6) →
    (∀ (n n_1 : ℕ) (a : α) (tail : List α) (has : n + 1 < (a :: tail).length) (hmn : n_1 + 1 ≤ n + 1),
        motive n.succ n_1.succ (a :: tail) has hmn) →
      motive x x_1 x_2 x_3 x_4