fact: Definition equiv_p1_1q {A : Type} {x y : A} {p q : x = y} : p = q <~> p @ 1 = 1 @ q := equiv_concat_lr (concat_p1 p) (concat_1p q)^.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics