Lemma mapSerializeSizeFromCombine : forall (vs : list componentValueT) (cs : list componentT),
  length vs = length cs ->
    componentValuesHaveTypes (combine vs cs) ->
      map (fun v => length (serializeValue v)) vs = map componentTypeSizeOctets (map componentType cs). 
Proof.
  (** Proof omitted for brevity. *)
Qed.
