proposition: Lemma oppnt_oppnt : forall u, oppnt (oppnt u) = u.
proof: Proof. ir. apply by_cases with (Nat_Trans.axioms u); ir. rw unfold_oppnt. rw unfold_oppnt. rww oppnt'_oppnt'. am. app oppnt_axioms. assert (oppnt u = u). uf oppnt. ap (Y_if_not H). tv. rw H0. am. Qed.
imports: Arith functor