Definition indexWithinBitRange (i : Z) (t : indexTypeT) : Prop :=
  match t with
  | INDEX_8  => 0 <= i /\ i < (2 ^ 8)
  | INDEX_16 => 0 <= i /\ i < (2 ^ 16)
  | INDEX_32 => 0 <= i /\ i < (2 ^ 32)
  end.
