fact: Definition equiv_cancelR {A} {x y z : A} (p q : x = y) (r : y = z) : (p @ r = q @ r) <~> (p = q) := equiv_inverse (equiv_whiskerR p q r).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics