proposition: Lemma cone_transform_vcompose : forall u v c, is_cone c -> cone_transformable v c -> Nat_Trans.axioms u -> source u = target v -> cone_transform (vcompose u v) c = cone_transform u (cone_transform v c).
proof: Proof. ir. uh H0; ee. uf cone_transform. rw vertex_cone_create. ap uneq. rw edge_nt_cone_create. rww vcompose_assoc. app edge_nt_axioms. Qed.
imports: Arith nat_trans