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