Definition fileWFIndexData (file : fileT) : Prop :=
  let info := fileInfo file in
  let shape := infoShape info in
    match shapeIndexInfo shape with
    | Some indexInfo =>
      let indexType := indexType indexInfo in
        match fileIndexData file with
        | Some indexData => indexArrayWF (Z.of_N (shapeElementCount shape)) (IndexArray indexType indexData)
        | None           => True
        end
    | None => True
    end.
