∀ {α : Type u_1} (motive : List α → Sort u_2) (x y : α) (xs : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → motive [x]) (h_3 : (x y : α) → (xs : List α) → motive (x :: y :: xs)),
  (match x :: y :: xs with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: y :: xs => h_3 x y xs) =
    h_3 x y xs