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