Theorem streamsWellFormedDivisible4 : ∀ es,
  streamWellFormed es → streamSize es mod 4 = 0.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
