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