{A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : q @ p^ = r <~> q = r @ p := Build_Equiv _ _ _ (isequiv_moveL_pM p q r). Global Instance isequiv_moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) : IsEquiv (moveL_Vp p q r). Proof. destruct r. apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.