Definition fileDescriptionInvariants (f : FileDescriptionT) : Prop :=
     fileSectionAtMostOneFirst (fileSections f)
  /\ fileSectionAtMostOneLast (fileSections f)
  /\ fileSectionTagsUnique (fileSections f)
  /\ fileSectionFileNotSection f
  /\ endSectionFileNotSection  f.
