∀ {α : Type u_1} (motive : (x x_1 : ℕ) → List α → x ≠ x_1 → Prop) (x x_1 : ℕ) (x_2 : List α) (x_3 : x ≠ x_1),
  (∀ (x x_4 : ℕ) (x_5 : x ≠ x_4), motive x x_4 [] x_5) →
    (∀ (n : ℕ) (head : α) (tail : List α) (x : n + 1 ≠ 0), motive n.succ 0 (head :: tail) x) →
      (∀ (n : ℕ) (head : α) (tail : List α) (x : 0 ≠ n + 1), motive 0 n.succ (head :: tail) x) →
        (∀ (n n_1 : ℕ) (head : α) (t : List α) (h : n + 1 ≠ n_1 + 1), motive n.succ n_1.succ (head :: t) h) →
          motive x x_1 x_2 x_3