Inductive FileDescriptionT := FileDescription {
  (** The file tag. *)
  fileTag             : TagT;
  (** The major file format version. *)
  fileVersionMajor    : nat;
  (** The minor file format version. *)
  fileVersionMinor    : nat;
  (** The file sections. *)
  fileSections        : list FileSectionDescriptionT;
  (** The file end tag. *)
  fileEndTag          : TagT;
  (** The constraints on unknown file sections. *)
  fileSectionsUnknown : FileSectionsUnknownT
}.
