{A} {x y z : A} (p q : x = y) (r : y = z) : IsEquiv (cancelR p q r). Proof. change (IsEquiv (equiv_cancelR p q r)); exact _. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.