Definition fileSectionFileNotSection (f : FileDescriptionT) : Prop :=
  ~In (fileTag f) (map (fun s => fileSectionTag s) (fileSections f)).
