proposition: Lemma vcompose_axioms : forall a b, axioms a -> axioms b -> source a = target b -> axioms (vcompose a b) = True.
proof: Proof. ir. app iff_eq; ir. clear H2. assert (osource a = osource b). uf osource; rw H1; nw. assert (otarget a = otarget b). uf otarget; wr H1; nw. uhg; ee. uf vcompose; ap create_like. nw. nw. nw. nw. nw. nw. sy; am. ir. nw. rww mor_comp. nw. rwi osource_vcompose H4. rww H2. nw. rwi osource_vcompose H4. am. nw. rww H1. rwi osource_vcompose H4. rww H2. rwi osource_vcompose H4; am. rwi osource_vcompose H4; am. ir. rwi osource_vcompose H4. cp H4. wri H2 H4. nw. cw. nw. nw. nw. nw. rww H1. ir. rwi osource_vcompose H4. cp H4; wri H2 H4. nw. cw. nw. nw. nw. nw. rww H1. ir. rwi osource_vcompose H4. cp H4; wri H2 H4. nw. rw assoc. rw H3. rw carre. wr assoc. wr assoc. app uncomp. wr H3. wr H1. rww carre. fw. nw. nw. sy; am. nw. cw. sy; am. nw. cw. fw. nw. cw. nw. nw. nw. rww H1. cw. cw. tv. nw. cw. sy; am. fw. nw. nw. nw. cw. nw. fw. rww H1. nw. nw. cw. nw. fw. nw. nw. cw. tv. am. am. nw. cw. nw. cw. fw. nw. nw. nw. rww H1. cw. cw. nw. fw. nw. cw. tv. cw. cw. Qed.
imports: Arith functor