fact: Definition pointwise_relation A {B} (R : relation B) : relation (A -> B) := fun f g => forall a, R (f a) (g a).
imports: Coq.Program.Basics Coq.Program.Tactics Coq.Relations.Relation_Definitions Coq.Classes.RelationClasses