proposition: Lemma vident_oppf1 : forall f, Functor.axioms f -> vident (oppf f) = oppnt' (vident f).
proof: Proof. ir. ap axioms_extensionality. rw vident_axioms. tv. app oppf_axioms. app oppnt'_axioms. rww vident_axioms. rw source_vident. rw source_oppnt'. rw target_vident. tv. rw target_vident. rw target_oppnt'. rw source_vident. tv. ir. cp H0. rwi osource_vident H0. rwi source_oppf H0. rwi ob_opp H0. rw ntrans_vident. rw ntrans_oppnt'. rw ntrans_vident. rw target_oppf. rw fob_oppf. rw id_opp. tv. rw ob_opp. ap ob_fob. am. am. am. rw source_oppf. rw ob_opp. am. am. am. am. rww vident_axioms. rw osource_vident. am. rw source_oppf. rw ob_opp. am. am. am. Qed.
imports: Arith functor