Theorem fileDescriptionInvariantsExample : fileDescriptionInvariants fileDescriptionExample.
