proposition: Lemma vcompose_assoc : forall a b c, axioms a -> axioms b -> axioms c -> source a = target b -> source b = target c -> vcompose (vcompose a b) c = vcompose a (vcompose b c).
proof: Proof. ir. ap axioms_extensionality; try am. rww vcompose_axioms. rww vcompose_axioms. nw. rww vcompose_axioms. rww vcompose_axioms. nw. rww source_vcompose. rww source_vcompose. rww source_vcompose. rw target_vcompose. rw target_vcompose. rw target_vcompose. tv. ir. rwi osource_vcompose H4. assert (otarget b = otarget a). uf otarget. wr H2. nw. assert (otarget c = otarget a). uf otarget. wr H3; nw. assert (osource b = osource a). uf osource. rw H2. nw. assert (osource c = osource a). uf osource. rw H2; nw. uf osource. rw H3. nw. rwi H8 H4. rww ntrans_vcompose. rww ntrans_vcompose. rw ntrans_vcompose. rw ntrans_vcompose. nw. rw assoc. rww H5. nw. nw. rww H7. sy; am. nw. rww H8. sy; am. nw. rww H2. rww H7. nw. rww H3. rww H7. rww H8. tv. rww H8. nw. rww H8. rww H7. rww H8. Qed.
imports: Arith functor