{A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) : q @ p = r <~> q = r @ p^ := Build_Equiv _ _ (moveL_pV p q r) _.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.