fact: Definition equiv_paths_ind `{Funext} {A : Type} (a : A) (P : forall x, (a = x) -> Type) : P a 1 <~> forall x p, P x p := Build_Equiv _ _ (paths_ind a P) _.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics