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. am. Qed.
imports: Arith functor