Theorem binaryEvalPaddedBytesU8 : forall bs a (Hnz : 0 <> a),
  Forall streamEIsU8 (binaryEvalPaddedBytes bs a Hnz).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
