proposition: Lemma target_colimit_to_cocone : forall a b, is_cocone a -> is_colimit b -> cosocle a = cosocle b -> target (colimit_to_cocone b a) = vertex a.
proof: Proof. ir. cp (colimit_to_cocone_pr H H0 H1). ee. transitivity (vertex (cocone_compose (colimit_to_cocone b a) b)). rw vertex_cocone_compose. tv. rw H3. tv. Qed.
imports: Arith limits