{G : Graph} {D : Diagram G} (P : Colimit D -> Type) (q : forall i x, P (colim i x)) (pp_q : forall (i j: G) (g: G i j) (x: D i), @colimp G D i j g x # q _ (D _f g x) = q _ x) (i j : G) (g : G i j) (x : D i) : apD (Colimit_ind P q pp_q) (colimp i j g x) = pp_q i j g x. Proof. refine (apD_V _ _ @ _). apply moveR_equiv_M. apply moveR_equiv_M. refine (Coeq_ind_beta_cglue _ _ _ _ @ _). symmetry. apply moveL_transport_p_V. Defined.
Require Import Basics Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.ConstantDiagram. Require Import Colimits.Coeq.