fact: Definition GraphQuotient_ind (P : GraphQuotient R -> Type@{k}) (gq' : forall a, P (gq a)) (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b) : forall x, P x := fun x => match x with | gq a => fun _ => gq' a end gqglue'.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath