fact: Definition Colimit_rec_beta_colimp {G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P) (i j : G) (g: G i j) (x: D i) : ap (Colimit_rec P C) (colimp i j g x) = legs_comm C i j g x.
imports: Basics Types Diagrams.Diagram Diagrams.Graph Diagrams.Cocone Diagrams.ConstantDiagram Colimits.Coeq