Theorem binaryEvalStreamsWellFormed : ∀ b,
  streamWellFormed (binaryEval b).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
