∀ {α : Type u_1} (motive : List α → ℕ → α → Sort u_2) (a : α) (as : List α) (n : ℕ) (b : α)
  (h_1 : (head : α) → (as : List α) → (b : α) → motive (head :: as) 0 b)
  (h_2 : (a : α) → (as : List α) → (n : ℕ) → (b : α) → motive (a :: as) n.succ b)
  (h_3 : (x : ℕ) → (x_1 : α) → motive [] x x_1),
  (match a :: as, n.succ, b with
    | head :: as, 0, b => h_1 head as b
    | a :: as, n.succ, b => h_2 a as n b
    | [], x, x_1 => h_3 x x_1) =
    h_2 a as n b