∀ {α : Type u_1} (motive : (x : List α) → (x_1 x_2 : ℕ) → x_1 + x_2 + 1 = x.length → Prop) (x : List α) (x_1 x_2 : ℕ)
  (x_3 : x_1 + x_2 + 1 = x.length),
  (∀ (x x_4 : ℕ) (x_5 : x + x_4 + 1 = [].length), motive [] x x_4 x_5) →
    (∀ (a : α) (l : List α) (i : ℕ) (h : i + 0 + 1 = (a :: l).length), motive (a :: l) i 0 h) →
      (∀ (a : α) (l : List α) (i j : ℕ) (h : i + (j + 1) + 1 = (a :: l).length), motive (a :: l) i j.succ h) →
        motive x x_1 x_2 x_3