Theorem streamSizeApp : forall xs ys,
  streamSize xs + streamSize ys = streamSize (xs ++ ys).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
