Inductive streamE : Set :=
  (** A 64-bit IEEE754 binary64 value. *)
  | Vf64 : R -> streamE
  (** A 64-bit unsigned integer. *)
  | Vu64 : nat -> streamE
  (** A 32-bit unsigned integer. *)
  | Vu32 : nat -> streamE
  (** An 8-bit unsigned integer. *)
  | Vu8  : nat -> streamE.
