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