∀ (motive : (x : ℕ) → BitVec x → Sort u_1) (w : ℕ) (x : BitVec (w + 1)) (h_1 : (x : BitVec 0) → motive 0 x)
  (h_2 : (w : ℕ) → (x : BitVec (w + 1)) → motive w.succ x),
  (match w.succ, x with
    | 0, x => h_1 x
    | w.succ, x => h_2 w x) =
    h_2 w x