fact: Definition cgraph_mor_comp {G H K : precgraph} (p : cgraph_mor G H) (q : cgraph_mor H K) : cgraph_mor G K := make_cgraph_mor (onnode q ∘ onnode p) (onarc q ∘ onarc p) (is_cgraph_mor_comp p q).
imports: UniMath.MoreFoundations.Propositions