∀ {α : Type u_1} (motive : List α → α → Sort u_2) (a : α) (as : List α) (x : α) (h_1 : (a₀ : α) → motive [] a₀)
  (h_2 : (a : α) → (as : List α) → (x : α) → motive (a :: as) x),
  (match a :: as, x with
    | [], a₀ => h_1 a₀
    | a :: as, x => h_2 a as x) =
    h_2 a as x