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