fact: Definition flatten_rec_beta_gqglue {Q : Type} (Qgq : forall a, F a -> Q) (Qgqglue : forall a b (r : R a b) (x : F a), Qgq a x = Qgq b (e _ _ r x)) (a b : A) (s : R a b) (x : F a) : ap (flatten_rec Qgq Qgqglue) (flatten_gqglue s x) = Qgqglue a b s x.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath