fact: Definition functor_forall_id `{P : A -> Type} `{Q : A -> Type} (f1 : forall a:A, P a -> Q a) : (forall a:A, P a) -> (forall a:A, Q a) := functor_forall idmap f1.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)