proposition: Lemma ntrans_oppnt' : forall u x, axioms u -> ob (osource u) x -> ntrans (oppnt' u) x = flip (ntrans u x).
proof: Proof. ir. uf oppnt'. rw ntrans_create. tv. rw source_oppf. ap ob_is_ob. rw ob_opp. rww source_target. rww functor_axioms_target. Qed.
imports: Arith functor