proposition: Lemma create_axioms : forall f g t, property f g t -> axioms (create f g t).
proof: Proof. ir. uf axioms. ee; ir; try (ap create_like); do 3 (first [rw osource_create| rw otarget_create| rw source_create| rw target_create| idtac]). uh H; ee. uh H; ee; am. uh H; ee. uh H0; ee; am. lu. lu. uh H; ee; sy; am. uh H; ee; am. rw ntrans_create. uh H; ee. ap H4. rwi osource_create H0. am. change (is_ob (source f) x). rwi osource_create H0. lu. rwi osource_create H0. rw ntrans_create. uh H; ee. au. change (is_ob (source f) x); lu. rwi osource_create H0. rw ntrans_create. uh H; ee. au. change (is_ob (source f) x); lu. rwi osource_create H0. rw ntrans_create. rw ntrans_create. uh H; ee. au. change (is_ob (source f) (source u)). assert (ob (source f) (source u)). cw. lu. change (is_ob (source f) (target u)). assert (ob (source f) (target u)). cw. lu. Qed.
imports: Arith functor