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