∀ (motive : List ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n),
  (match [], x with
    | [], x => h_1 x
    | m :: l, n => h_2 m l n) =
    h_1 x