fact: Definition flatten_gqglue {x y} (s : R x y) (a : F x) : flatten_gq a = flatten_gq (e x y s a).
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath