proposition: Lemma opp'_axioms : forall a, axioms a -> axioms (opp' a).
proof: Proof. ir. assert (morli : forall u, is_mor a u -> Arrow.like u). ir. uh H; ee. rwi H1 H0. uh H0; ee. am. assert (obidli : forall x, is_ob a x -> Arrow.like (id a x)). ir. uh H. ee. rwi H H0. uh H0. ee. ap morli. am. assert (flifli : forall u, flip (flip u) = u). ir. rw flip_flip. tv. uf opp'. ap create_axioms. assert (ax : axioms a). am. uh H; ee. assert (alike : like a). am. clear H3. uhg; dj; try (ap iff_eq; ir). assert (ob a x). apply is_ob_ob. am. am. uhg; ee. am. ap Image.show_inc. sh (id a x). ee. ap mor_is_mor. ap mor_id. ap is_ob_ob. am. am. tv. rw source_flip. rww target_id. ap obidli. am. rw target_flip. rww source_id. app obidli. lu. assert (mor a (flip u)). rwi Image.inc_rw H4. nin H4; ee. ap is_mor_mor. am. wr H5. rw flip_flip. am. uhg; ee. am. wr (flifli u). rw source_flip. uh H5; ee. rwi H0 H6. lu. ap morli. lu. wr source_flip. ap ob_is_ob. rww ob_source. rw like_flip. ap morli. lu. rw flip_flip. rw left_id. rww flip_flip. wr target_flip. rww ob_target. rw like_flip. ap morli. lu. am. rww target_flip. rw like_flip. ap morli. lu. tv. rw flip_flip. rw right_id. rww flip_flip. wr source_flip. rww ob_source. rw like_flip. ap morli. lu. am. rww source_flip. rw like_flip. ap morli. lu. tv. rw like_flip. ap morli. lu. lu. assert (mor a (flip u)). rwi Image.inc_rw H5. nin H5; ee. wr H8. rw flip_flip. app is_mor_mor. assert (mor a (flip v)). rwi Image.inc_rw H6. nin H6; ee. wr H9. rw flip_flip. app is_mor_mor. assert (Arrow.like u). rw like_flip. ap morli. ap mor_is_mor. am. assert (Arrow.like v). rw like_flip. ap morli. ap mor_is_mor. am. uhg; ee. am. am. am. ap Image.show_inc. sh (comp a (flip v) (flip u)). ee. ap mor_is_mor. rw mor_comp. tv. am. am. rw source_flip. rw target_flip. sy; am. rw like_flip. ap morli. ap mor_is_mor. tv. rw like_flip. ap morli. ap mor_is_mor. am. tv. tv. rw source_flip. rw target_comp. rww target_flip. am. am. rw source_flip. rw target_flip. sy; am. am. am. ap morli. ap mor_is_mor. rw mor_comp. tv. am. am. rw source_flip. rw target_flip. sy; am. tv. am. tv. rw target_flip. rw source_comp. rww source_flip. am. am. rw source_flip. rww target_flip. sy; am. am. ap morli. ap mor_is_mor. rw mor_comp. tv. am. am. rww source_flip. rww target_flip. sy; am. tv. rw flip_flip. rw flip_flip. assert (mor a (flip u)). rwi Image.inc_rw H6. nin H6; ee. wr H11. rw flip_flip. app is_mor_mor. assert (mor a (flip v)). rwi Image.inc_rw H7. nin H7; ee. wr H12. rw flip_flip. app is_mor_mor. assert (mor a (flip w)). rwi Image.inc_rw H8. nin H8; ee. wr H13. rw flip_flip. app is_mor_mor. assert (Arrow.like u). rw like_flip. ap morli. ap mor_is_mor. am. assert (Arrow.like v). rw like_flip. ap morli. ap mor_is_mor. am. assert (Arrow.like w). rw like_flip. ap morli. ap mor_is_mor. am. rw assoc. tv. am. am. am. rww source_flip. rww target_flip. sy; am. sy; rww source_flip; rww target_flip. tv. Qed.
imports: Arith universe