(a : A) (b' : B') : ap (Coeq_rec2 (coeq a)) (cglue b') = cgluer a b'. Proof. nrapply Coeq_rec_beta_cglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.