proposition: Lemma fob_opp_fc : forall a b x, Category.axioms a -> Category.axioms b -> ob (opp (functor_cat a b)) x -> fob (opp_fc a b) x = oppf x.
proof: Proof. ir. uf fob. rw fmor_opp_fc. rw source_opp_fc. rw source_oppnt. rw target_flip. rw source_id. tv. am. apply mor_arrow_like with (opp (functor_cat a b)). ap mor_id. am. rw id_opp. rw flip_flip. rw id_functor_cat. rww vident_axioms. rwi ob_opp H1. rwi ob_functor_cat H1. uh H1; ee; am. am. am. am. am. rwi ob_opp H1. am. am. rw source_opp_fc. ap mor_id. am. Qed.
imports: Arith nat_trans