proposition: Lemma cocone_transform_vcompose : forall u v c, is_cocone c -> cocone_transformable c v -> Nat_Trans.axioms u -> source v = target u -> cocone_transform c (vcompose v u) = cocone_transform (cocone_transform c v) u.
proof: Proof. ir. uh H0; ee. uf cocone_transform. rw vertex_cocone_create. ap uneq. rw coedge_nt_cocone_create. rww vcompose_assoc. app coedge_nt_axioms. rww source_coedge_nt. sy; am. Qed.
imports: Arith limits