proposition: Lemma hcompose_vident_right : forall a f, axioms a -> Functor.axioms f -> target f = osource a -> hcompose a (vident f) = htrans_right a f.
proof: Proof. ir. ap axioms_extensionality. ap hcompose_axioms. uhg; ee. nw. nw. nw. nw. nw. nw. nw. ir. nw. ir. nw. ir. nw. ir. rw carre. tv. am. am. rww vident_axioms. nw. sy; am. ap htrans_right_axioms. am. am. sy; am. rw source_hcompose. rw source_htrans_right. rw source_vident. tv. rw target_hcompose. rw target_vident. rw target_htrans_right. tv. ir. rwi osource_hcompose H2. rwi osource_vident H2. rww ntrans_hcompose. rww ntrans_vident. rww ntrans_htrans_right. rww target_vident. rww fmor_id. rw target_source. rw right_id. tv. fw. nw. nw. wr H1. fw. nw. nw. wr H1; fw. nw. wr H1; fw. tv. am. nw. sy; am. fw. uhg; ee. am. rww vident_axioms. rw otarget_vident. sy; am. rww osource_vident. Qed.
imports: Arith functor