Lemma binaryExpOctetsSum2 : forall (x y : binaryExp),
  List.length (binaryExpOctets x ++ binaryExpOctets y) =
    List.length (binaryExpOctets x) + List.length (binaryExpOctets y).
Proof.
  (** Proof omitted for brevity. *)
Qed.
