Inductive FileSectionCardinalityT :=
    (** The section must appear exactly once. *)
    FSC_One
  | (** The section can appear at most once. *)
    FSC_ZeroToOne
  | (** The section can appear any number of times, including not at all. *)
    FSC_ZeroToN
  | (** The section must appear at least once. *)
    FSC_OneToN
  .
