proposition: Lemma htrans_right_axioms : forall f a, Functor.axioms f -> axioms a -> osource a = target f -> axioms (htrans_right a f).
proof: Proof. ir. uhg; ee. uf htrans_right; ap create_like. rw osource_htrans_right. fw. rw otarget_htrans_right. nw. rw source_htrans_right. fw. nw. rw target_htrans_right. fw. nw. nw. rw target_htrans_right. rw source_fcompose. rw osource_htrans_right. tv. rw source_htrans_right. rw target_fcompose. rw otarget_htrans_right. nw. ir. rwi osource_htrans_right H2. rw otarget_htrans_right. rw ntrans_htrans_right. nw. fw. am. ir. rwi osource_htrans_right H2. rw ntrans_htrans_right. rw source_ntrans. rw source_htrans_right. rww fob_fcompose. nw. am. fw. am. ir. rwi osource_htrans_right H2. rw ntrans_htrans_right. rw target_ntrans. rw target_htrans_right. rww fob_fcompose. nw. nw. am. fw. am. ir. rwi osource_htrans_right H2. rw otarget_htrans_right. rw ntrans_htrans_right. rw source_htrans_right. rw target_htrans_right. rw ntrans_htrans_right. rw fmor_fcompose. rw fmor_fcompose. wr target_fmor. wr source_fmor. rw carre. tv. am. fw. am. am. am. am. nw. am. nw. am. nw. am. nw. am. cw. cw. Qed.
imports: Arith functor