fact: Definition R_arrow {A A' : Type} (PA : Param00.Rel A A') {B B' : Type} (PB : Param00.Rel B B') : (A -> B) -> (A' -> B') -> Type := fun f f' => forall a a', PA a a' -> PB (f a) (f' a').
imports: elpi(elpi) Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy