proposition: Lemma fcompose_oppf : forall f g, Functor.axioms f -> Functor.axioms g -> source f = target g -> fcompose (oppf f) (oppf g) = oppf (fcompose f g).
proof: Proof. ir. rww unfold_oppf. rww unfold_oppf. rw unfold_oppf. rww fcompose_oppf'. app fcompose_axioms. Qed.
imports: Arith category