proposition: Lemma oppf_constant_functor : forall a b x, Category.axioms a -> ob b x -> oppf (constant_functor a b x) = constant_functor (opp a) (opp b) x.
proof: Proof. ir. rw unfold_oppf. rww oppf'_constant_functor. ap constant_functor_axioms. am. uh H0; ee; am. am. Qed.
imports: Arith category