∀ {n : ℕ} (motive : (x x_1 : BitVec n) → x.toNat = x_1.toNat → Prop) (x x_1 : BitVec n) (x_2 : x.toNat = x_1.toNat),
  (∀ (val : ℕ) (isLt isLt_1 : val < 2 ^ n), motive { toFin := ⟨val, isLt⟩ } { toFin := ⟨val, isLt_1⟩ } ⋯) →
    motive x x_1 x_2