Definition indexArrayWF (dataSize : Z) (i : indexArrayT) : Prop :=
     indexArrayWFElementsNonEmpty i
  /\ indexArrayWFElementsLtDataSize dataSize i
  /\ indexArrayWFElementsBitRange i.
