Definition indexArrayWFElementsBitRange (i : indexArrayT) : Prop :=
  Forall (fun e => indexWithinBitRange e (indexElementType i)) (indexElements i).
