{x y} (s : R x y) (a : F x) : flatten_gq a = flatten_gq (e x y s a). Proof. snrapply path_sigma'. - by apply gqglue. - apply transport_DGraphQuotient. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.