proposition: Lemma vcompose_htrans_right_htrans_right : forall u v f g, axioms u -> axioms v -> Functor.axioms f -> f = g -> source u = target v -> target f = osource u -> vcompose (htrans_right u f) (htrans_right v g) = htrans_right (vcompose u v) f.
proof: Proof. ir. assert (osource u = osource v). uf osource. rw H3. rw source_target. tv. am. cp hcompose_vident_right. wr H2. util (H6 u f). am. am. am. util (H6 v f). am. am. wr H5; am. util (H6 (vcompose u v) f). rww vcompose_axioms. am. rww osource_vcompose. wrr H5. wr H7. wr H8. assert (vident f = vcompose (vident f) (vident f)). rw weak_left_vident. reflexivity. rww vident_axioms. rww target_vident. rwi H10 H9. wr H9. apply interchange. rww target_vident. rww source_vident. sy; am. rww otarget_vident. sy; wrr H5. rww vident_axioms. am. rww vident_axioms. am. Qed.
imports: Arith functor