Lemma fileSectionAtMostOneFirstExample : fileSectionAtMostOneFirst (fileSections fileDescriptionExample).
