proposition: Lemma vcompose_htrans_left_htrans_left : forall u v f g, axioms u -> axioms v -> Functor.axioms f -> f = g -> source u = target v -> source f = otarget u -> vcompose (htrans_left f u) (htrans_left g v) = htrans_left f (vcompose u v).
proof: Proof. ir. assert (otarget u = otarget v). uf otarget. wr H3. rw target_source. tv. am. cp hcompose_vident_left. wr H2. util (H6 f u). am. am. am. util (H6 f v). am. am. wr H5; am. util (H6 f (vcompose u v)). rww vcompose_axioms. am. rww otarget_vcompose. 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. sy; am. rww target_vident. rww source_vident. rww osource_vident. sy; wrr H5. sy; am. am. rww vident_axioms. am. rww vident_axioms. Qed.
imports: Arith functor