{A : Type} `{Is1Gpd A} {x y : A} {p q : x $-> y} (r : p $== q) : p^$ $== q^$. Proof. apply gpd_moveR_V1. apply gpd_moveL_hV. exact (cat_idl q $@ r^$). Defined.
Require Import Basics.Overture Basics.Tactics.