fact: Definition path_forall_pp `{P : A -> Type} (f g h : forall x, P x) (p : f == g) (q : g == h) : path_forall f h (fun x => p x @ q x) = path_forall f g p @ path_forall g h q.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)