proposition: Lemma mor_colimit_to_cocone : forall a b y, is_cocone a -> is_colimit b -> cosocle a = cosocle b -> y = cocone_target b -> mor y (colimit_to_cocone b a).
proof: Proof. ir. cp (colimit_to_cocone_pr H H0 H1). ee. uh H3; ee. rw H2; am. Qed.
imports: Arith limits