Definition fileWF (file : fileT) : Prop :=
     fileWFIndexDataPresentIff file
  /\ fileWFIndexData file
  /\ fileWFDataLength file
  /\ fileWFDataTyped file
  /\ infoWF (fileInfo file).
