Theorem serializedStructureValueSizeCorrect : forall sv st,
  structureValueHasStructureType sv st ->
    length (serializeStructureValue sv) = structureSizeOctets st.
Proof.
  (** Proof omitted for brevity. *)
Qed.
