{A} `{Is1Gpd A} {a : A} : (Id a)^$ $== Id a. Proof. refine ((gpd_rev2 (gpd_issect (Id a)))^$ $@ _). refine (gpd_rev_pp _ _ $@ _). apply gpd_isretr. Defined.
Require Import Basics.Overture Basics.Tactics.