proposition: Lemma oppf_oppf : forall f, oppf (oppf f) = f.
proof: Proof. ir. apply by_cases with (Functor.axioms f); ir. rw unfold_oppf. rw unfold_oppf. rww oppf'_oppf'. am. app oppf_axioms. assert (oppf f = f). uf oppf. ap (Y_if_not H). tv. rw H0. am. Qed.
imports: Arith category