fact: Definition cocone_precompose_postcompose {D1 D2 : Diagram G} (m : DiagramMap D1 D2) `(f : X -> Y) (C : Cocone D2 X) : cocone_postcompose (cocone_precompose m C) f = cocone_precompose m (cocone_postcompose C f).
imports: Basics Types Diagrams.Graph Diagrams.Diagram