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