∀ (motive : ℕ → ℕ → List ℕ → Sort u_1) (x : ℕ) (acc : List ℕ) (h_1 : (x : ℕ) → (acc : List ℕ) → motive 0 x acc)
  (h_2 : (n e : ℕ) → (acc : List ℕ) → motive n.succ e acc),
  (match 0, x, acc with
    | 0, x, acc => h_1 x acc
    | n.succ, e, acc => h_2 n e acc) =
    h_1 x acc