∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_2 ()