proposition: Lemma osource_oppnt' : forall u, axioms u -> osource (oppnt' u) = opp (osource u).
proof: Proof. ir. uf osource. rw source_oppnt'. rw source_oppf. rww source_target. rww functor_axioms_target. Qed.
imports: Arith functor