proposition: Lemma htrans_right_vident : forall f g, Functor.axioms f -> Functor.axioms g -> source f = target g-> htrans_right (vident f) g = vident (fcompose f g).
proof: Proof. ir. wr hcompose_vident_right. rw hcompose_vident_vident. tv. am. am. am. rww vident_axioms. am. nw. sy; am. Qed.
imports: Arith functor