Lemma fileDescription1InvariantsAtMostOneFirst : fileSectionAtMostOneFirst (fileSections fileDescription1).
