proposition: Lemma create_axioms : forall o m (c : E2) (i:E1) (s:E), property o m c i -> axioms (create o m c i s).
proof: Proof. ir. set (k:=(create o m c i s)). assert (lem1 : forall u v, are_composable k u v = (inc u m & inc v m & source u = target v)). ir. ap iff_eq; ir. ufi k H0. rwi are_composable_create_rw H0. xd. uf k. rw are_composable_create_rw. xd. uh H; ee. assert (lem2: forall u, is_mor k u = inc u m). ir. ap iff_eq; ir. ufi k H3. rwi is_mor_create H3. am. uf k; rw is_mor_create; am. assert (lem3: forall u v, inc u m -> inc v m -> source u = target v -> comp k u v = c u v). ir. uf k. rw comp_create; tv. assert (lem5: forall x, inc x o -> id k x = i x). ir. uf k. rw id_create. tv. am. assert (lem6: forall (x:E), is_ob k x = inc x o). ir; ap iff_eq; ir. ufi k H3. rwi is_ob_create H3. am. uf k; rw is_ob_create; am. uhg; ee; ir. ap iff_eq; ir. cp H3; rwi lem6 H3. rwi H H3. uh H3; ee. uhg; dj. am. rw lem2. rw lem5. am. am. rw lem5; am. rw lem5; am. rw lem5. rw lem3. rwi lem2 H12. rwi H0 H12. uh H12; ee. wr H13. am. wr lem2. am. wr lem5. wr lem2. am. am. rw H7. am. am. rw lem3. rw lem5. rwi lem2 H13. rwi H0 H13. uh H13; ee. wr H14. am. lu. wr lem2. am. wr lem2. am. rw H10. sy; am. lu. ap iff_eq; ir. rwi lem2 H3. rwi H0 H3. uh H3; ee. uhg; ee. rw lem2; am. rw lem6; am. rw lem6; am. rw lem3. rw lem5. am. am. rww lem5. rwi H H5. lu. am. rww lem5. rwi H0 H3. uh H3; ee. rwi H H10. uh H10; ee. am. rww lem3. rw lem5. am. am. rw lem5. rwi H H4. uh H4; ee. am. am. rw lem5. rwi H H4. uh H4; ee. sy; am. am. am. lu. ap iff_eq; ir. cp H3; uh H3; ee. rwi lem2 H3. rwi lem2 H5. util (H1 u v). am. am. am. uh H7; ee. uhg; xd. rw lem2. rww lem3. rww lem3. rww lem3. lu. assert (inc u m). wr lem2; lu. assert (inc v m). wr lem2; lu. assert (inc w m). wr lem2; lu. assert (source u = target v). lu. assert (source v = target w). lu. rww lem3. rww lem3. rww lem3. rww lem3. rwi lem1 H3; rwi lem1 H4; ee. ap H2; try am. rww lem3. cp (H1 _ _ H6 H7 H9). lu. rww lem3. cp (H1 _ _ H5 H6 H8). util (H1 v w). am. am. am. uh H11; ee. rw H16. am. util (H1 u v). am. am. am. rw lem3. uh H10; ee. am. am. am. am. rww lem3. util (H1 u v). am. am. am. uh H10; ee. rw H14. am. uf k. ap create_like. Qed.
imports: Arith universe