proposition: Lemma hcompose_vident_vident : forall f g, Functor.axioms f -> Functor.axioms g -> source f = target g -> hcompose (vident f) (vident g) = vident (fcompose f g).
proof: Proof. ir. rw hcompose_vident_left. ap axioms_extensionality. ap htrans_left_axioms. am. rww vident_axioms. rww otarget_vident. rww vident_axioms. app fcompose_axioms. rw source_htrans_left. rw source_vident. rw source_vident. tv. rw target_htrans_left. rw target_vident. rw target_vident. tv. ir. rwi osource_htrans_left H2. rwi osource_vident H2. rw ntrans_htrans_left. rw ntrans_vident. rw ntrans_vident. rw target_fcompose. rw fmor_id. ap uneq. rww fob_fcompose. am. am. fw. fw. am. nw. rww vident_axioms. am. nw. Qed.
imports: Arith functor