{A : Type} `{Is1Gpd A} {x y : A} {p q : x $-> y} (r : Id _ $== p^$ $o q) : p $== q. Proof. refine (_ $@ (cat_assoc _ _ _)^$ $@ ((gpd_isretr p) $@R q) $@ (cat_idl q)). exact ((cat_idr p)^$ $@ (p $@L r)). Defined.
Require Import Basics.Overture Basics.Tactics.