proposition: Lemma oppf'_fidentity : forall a, Category.axioms a -> oppf' (fidentity a) = fidentity (opp a).
proof: Proof. ir. assert (Category.axioms (opp a)). app opp_axioms. assert (axioms (oppf' (fidentity a))). app oppf'_axioms. rww fidentity_axioms. ap axioms_extensionality. am. rww fidentity_axioms. rww source_oppf'. rww source_fidentity. rww source_fidentity. rww target_oppf'. rww target_fidentity. rww target_fidentity. ir. cp H2. rwi source_oppf' H3. cp H3. rwi mor_opp H4. rwi source_fidentity H4. rw fmor_oppf'. rw fmor_fidentity. rw fmor_fidentity. rww flip_flip. rw mor_opp. am. am. am. Qed.
imports: Arith category