Definition fileSectionInfo : FileSectionDescriptionT :=
  FileSectionDescription
    (tagOfZ (Z.of_N infoSectionIdentifier))
    FSO_MustBeFirst
    FSC_One.
