{A} `{Is1Gpd A} {a b c : A} (f : b $-> c) (g : a $-> b) : (f $o g)^$ $== g^$ $o f^$. Proof. apply gpd_moveR_V1. refine (_ $@ cat_assoc _ _ _). apply gpd_moveL_hV. refine (cat_idl _ $@ _). exact (gpd_hh_V _ _)^$. Defined.
Require Import Basics.Overture Basics.Tactics.