∀ {α : Type u_1} (motive : List ℕ → List α → Sort u_2) (n : ℕ) (ns : List ℕ) (x : List α)
  (h_1 : (x : List α) → motive [] x) (h_2 : (n : ℕ) → (ns : List ℕ) → (x : List α) → motive (n :: ns) x),
  (match n :: ns, x with
    | [], x => h_1 x
    | n :: ns, x => h_2 n ns x) =
    h_2 n ns x