{A : Type} `(p : x = y) (z : A) : (y = z) <~> (x = z) := Build_Equiv _ _ (concat p) _. Global Instance isequiv_concat_r {A : Type} `(p : y = z) (x : A) : IsEquiv (fun q:x=y => q @ p) | 0. Proof. refine (Build_IsEquiv _ _ (fun q => q @ p) (fun q => q @ p^) (fun q => concat_pV_p q p) (fun q => concat_pp_V q p) _). intros q; destruct p; destruct q; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.