∀ {α : Type u_1} (motive : ℕ → List α → α → Sort u_2) (x : List α) (x_1 : α)
  (h_1 : (x : List α) → (x_2 : α) → motive 0 x x_2) (h_2 : (n : ℕ) → (l : List α) → (x : α) → motive n.succ l x),
  (match 0, x, x_1 with
    | 0, x, x_2 => h_1 x x_2
    | n.succ, l, x => h_2 n l x) =
    h_1 x x_1