fact: Definition apD10_path_forall `{P : A -> Type} (f g : forall x, P x) (h : f == g) : apD10 (path_forall _ _ h) == h := apD10 (eisretr apD10 h).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)