proposition: Lemma create_axioms : forall a b (fm:E1), (exists fo, property a b fo fm) -> axioms (create a b fm).
proof: Proof. ir. uhg. do 50 (try (rw source_create)). do 50 (try (rw target_create)). do 50 (try (rw fmor_create)). nin H. ee; ir; try (rw fmor_create); try (rw (fob_property_create (a:= a) (b:=b) (fo := x) (fm := fm))). uf create. ap Umorphism.create_like. lu. lu. uh H; ee. app H2. am. am. uh H; ee. app H3. am. am. cw. uh H; ee. app H4. am. uh H; ee. app H5. am. cw. am. uh H; ee. app H6. am. cw. am. rww fmor_create. rww fmor_create. uh H; ee. rww H9. cw. am. Qed.
imports: Arith category