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