∀ (motive : List ℕ → Sort u_1) (h : ℕ) (t : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (h : ℕ) → (t : List ℕ) → motive (h :: t)),
  (match h :: t with
    | [] => h_1 ()
    | h :: t => h_2 h t) =
    h_2 h t