Lemma fileDescription1InvariantsAtMostOneLast : fileSectionAtMostOneLast (fileSections fileDescription1).
