Lemma repeat_eq : forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
  Forall (eq x) (repeat x n).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
