fact: Definition equiv_path_ind {A} {a : A} {X : A -> Type} (e : forall (b : A), a = b <~> X b) (P : forall (b : A), X b -> Type) (r : P a (e a 1)) : forall (b : A) (x : X b), P b x.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics