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