Lemma Forall_implies : forall (A : Type) (P : A -> Prop) (Q : A -> Prop) (xs : list A) (H : forall x, P x -> Q x),
  Forall P xs -> Forall Q xs.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
