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