proposition: Lemma vcompose_oppnt : forall u v, Nat_Trans.axioms u -> Nat_Trans.axioms v -> source u = target v -> vcompose (oppnt v) (oppnt u) = oppnt (vcompose u v).
proof: Proof. ir. rww unfold_oppnt. rww unfold_oppnt. rww vcompose_oppnt'. rww unfold_oppnt. rww vcompose_axioms. Qed.
imports: Arith functor