fact: Definition equiv_path_forall `{P : A -> Type} (f g : forall x, P x) : (f == g) <~> (f = g) := Build_Equiv _ _ (path_forall f g) _.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)