proposition: Lemma otarget_oppnt' : forall u, axioms u -> otarget (oppnt' u) = opp (otarget u).
proof: Proof. ir. uf otarget. rw target_oppnt'. rw target_oppf. rww target_source. rww functor_axioms_source. Qed.
imports: Arith functor