Lemma fileDescription1InvariantsTagsUnique : fileSectionTagsUnique (fileSections fileDescription1).
