Lemma app_cons : forall (A : Type) (x : A) (xs : list A),
  x :: xs = app (cons x nil) xs.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
