Definition indexArrayWFElementsLtDataSize (dataSize : Z) (i : indexArrayT) : Prop :=
  Forall (fun e => 0 <= e /\ e < dataSize) (indexElements i).
