`{Funext} {A : Type} (a : A) (P : forall x, (x = a) -> Type) : P a 1 <~> forall x p, P x p := Build_Equiv _ _ (paths_ind_r a P) _.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.