proposition: Lemma hcompose_vident_left : forall f a, axioms a -> Functor.axioms f -> source f = otarget a -> hcompose (vident f) a = htrans_left f a.
proof: Proof. ir. ap axioms_extensionality. ap hcompose_axioms. rw vident_axioms. tv. am. am. nw. app htrans_left_axioms. rww source_hcompose. rw source_htrans_left. rw source_vident. tv. rw target_hcompose. rw target_vident. rw target_htrans_left. tv. ir. rwi osource_hcompose H2. rw ntrans_hcompose. rw ntrans_htrans_left. rw otarget_vident. rw ntrans_vident. rw left_id. rw source_vident. tv. ap ob_fob. am. rw H1. uf otarget. ap ob_fob. nw. nw. nw. fw. nw. nw. rw target_fmor. rw target_ntrans. tv. am. am. am. nw. tv. fw. nw. nw. am. uhg; ee. rww vident_axioms. am. nw. am. Qed.
imports: Arith functor