Definition fileWFIndexDataPresentIff (file : fileT) : Prop :=
  shapeIndexInfo (infoShape (fileInfo file)) <> None <-> fileIndexData file <> None.
