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