fact: Definition ap (X Y Z : RSetoid) : (X --> Y --> Z) --> (X --> Y) --> (X --> Z) := compose (compose (compose (@join _ _)) (@flip _ _ _)) (compose (@compose _ _ _)).
imports: Coq.Setoids.Setoid (hints) MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra