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