Definition fileWFDataLength (f : fileT) : Prop :=
  length (fileData f) = N.to_nat (shapeElementCount (infoShape (fileInfo f))).
