fact: Definition equiv_moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) : (p = r @ q) <~> (r^ @ p = q) := Build_Equiv _ _ (moveR_Vp p q r) _.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics