proposition: Lemma create_strong_axioms : forall (x y : E) (f : E1), property x y f -> strong_axioms (create x y f).
proof: Proof. ir. unfold strong_axioms in |- *. ee. unfold axioms in |- *. rw source_create. rw target_create. uf property. uf Transformation.axioms. ir. rw ev_create. ufi property H. ufi Transformation.axioms H. ap H. am. am. ap create_like. Qed.
imports: Arith functions