fact: Definition forall_relation (P : A -> Type) (sig : forall a, crelation (P a)) : crelation (forall x, P x) := fun f g => forall a, sig a (f a) (g a).
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Classes.CRelationClasses