proposition: Lemma opp'_opp' : forall a, axioms a -> opp' (opp' a) = a.
proof: Proof. ir. assert (like a). lu. uh H0. transitivity (create (objects a) (morphisms a) (comp a) (id a) (structure a)). assert (Image.create (Image.create (morphisms a) flip) flip = morphisms a). ap extensionality; uhg; ir. rwi Image.inc_rw H1. nin H1. ee. rwi Image.inc_rw H1. nin H1. ee. wr H2. wr H3. rw flip_flip. am. ap Image.show_inc. sh (flip x). ee. ap Image.show_inc. sh x. ee. am. tv. rww flip_flip. uf opp'. ap create_extensionality. rww objects_create. rw morphisms_create. am. rw morphisms_create. rw H1. ir. rw comp_create. rw flip_flip. rw flip_flip. rww flip_flip. ap Image.show_inc. sh v; ee; try am. tv. ap Image.show_inc. sh u; ee; try tv; try am. rw source_flip. rw target_flip. sy; am. apply mor_arrow_like with a. app is_mor_mor. apply mor_arrow_like with a. app is_mor_mor. rw objects_create. ir. rw id_create. rww flip_flip. am. rww structure_create. sy; am. Qed.
imports: Arith universe