Definition fileSectionIndex : FileSectionDescriptionT :=
  FileSectionDescription
    (tagOfZ (Z.of_N indexSectionIdentifier))
    FSO_AnyOrder
    FSC_ZeroToOne.
