Inductive streamWellFormed : list streamE -> Prop :=
  (** An empty stream is well-formed. *)
  | BEPEmpty  : streamWellFormed []
  (** A stream consisting of a single 64-bit float is well-formed. *)
  | BEPVf64   : forall k, streamWellFormed [Vf64 k]
  (** A stream consisting of a single 64-bit integer is well-formed. *)
  | BEPVu64   : forall k, streamWellFormed [Vu64 k]
  (** A stream consisting of a single 32-bit integer is well-formed. *)
  | BEPVu32   : forall k, streamWellFormed [Vu32 k]
  (** A stream consisting of a number of 8-bit values of a length divisible by 4 is well-formed. *)
  | BEPVu8s   : forall es, Forall streamEIsU8 es -> length (es) mod 4 = 0 -> streamWellFormed es
  (** The concatenation of two well-formed streams is well-formed. *)
  | BEPAppend : forall xs ys, streamWellFormed xs -> streamWellFormed ys -> streamWellFormed (xs ++ ys).
