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