Lemma metadataSectionSize : forall s,
  lengthN (binaryExpsNamedOctets (metadataSection s)) mod 16 = 0.
Proof.
  (** Proof omitted for brevity. *)
Qed.
