(a : A) (a' : A') : Coeq_rec2 (coeq a) (coeq a') = coeq' a a' := 1.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.