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