∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : n.succ = 0 → motive 0) (h_2 : (n_1 : ℕ) → n.succ = n_1.succ → motive n_1.succ),
  (match cardeq : n.succ with
    | 0 => h_1 cardeq
    | n_1.succ => h_2 n_1 cardeq) =
    h_2 n ⋯