proposition: Lemma htrans_left_axioms : forall f a, Functor.axioms f -> axioms a -> source f = otarget a -> axioms (htrans_left f a).
proof: Proof. ir. uhg; ee. uf htrans_left. ap create_like. rw osource_htrans_left. nw. rww otarget_htrans_left. fw. rww source_htrans_left. fw. nw. nw. rw target_htrans_left. fw. nw. rw osource_htrans_left. rw target_htrans_left. rw source_fcompose. nw. rw source_htrans_left. rw target_fcompose. rww otarget_htrans_left. ir. rwi osource_htrans_left H2. rw otarget_htrans_left. rw ntrans_htrans_left. fw. nw. am. ir. rwi osource_htrans_left H2. rw ntrans_htrans_left. rw source_fmor. rw source_htrans_left. rw source_ntrans. rw fob_fcompose. tv. am. nw. nw. nw. am. am. am. nw. am. ir. rwi osource_htrans_left H2. rww ntrans_htrans_left. rww target_htrans_left. rww target_fmor. rww target_ntrans. rww fob_fcompose. nw. nw. nw. ir. rwi osource_htrans_left H2. rw otarget_htrans_left. rw ntrans_htrans_left. rw target_htrans_left. rw ntrans_htrans_left. rw fmor_fcompose. rw source_htrans_left. rw fmor_fcompose. rw comp_fmor. rw comp_fmor. ap uneq. rw H1. rww carre. am. fw. nw. nw. nw. cw. nw. fw. nw. nw. cw. am. nw. cw. fw. nw. nw. nw. fw. nw. cw. am. nw. nw. nw. am. nw. nw. nw. cw. cw. Qed.
imports: Arith functor