Lemma app_list_implies_eq : forall (A : Type) (x y : A) (xs : list A),
  xs ++ [x] = [y] -> xs = [] /\ x = y.
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.
