Theorem indexWithinBitRangeDecidable : forall i t,
  {indexWithinBitRange i t}+{~indexWithinBitRange i t}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
