fact: Definition forall_relation (sig : forall a, relation (P a)) : relation (forall x, P x) := fun f g => forall a, sig a (f a) (g a).
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses