proposition: Lemma forall_subrelation (R S : forall x : A, relation (P x)) : (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).
proof: Proof. intros H x y H0 a. apply H. apply H0. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses