Lemma endSectionSize : length (binaryExpsNamedOctets endSection) = 16%nat.
