Lemma infoSectionSize : forall i,
  lengthN (binaryExpsNamedOctets (infoSection i)) mod 16 = 0.
Proof.
  (** Proof omitted for brevity. *)
Qed.
