proposition: Lemma forall_subrelation (P : A -> Type) (R S : forall x : A, crelation (P x)) : (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation P R) (forall_relation P S).
proof: Proof. reduce. firstorder. Qed.
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses