Lemma binaryExpsOctetsAppend : forall (xs ys : list binaryExp),
  binaryExpsOctets xs ++ binaryExpsOctets ys = binaryExpsOctets (xs ++ ys).
Proof.
  (** Proof omitted for brevity. *)
Qed.
