proposition: Lemma create_axioms : forall (a : E) (l : E2P), property a l -> axioms (create a l).
proof: Proof. ir. uf axioms. dj. cluc. ap leq_create_if; try am. ufi property H. ee. ap H; am. ufi leq H1. xe. ufi leq H2; xe. assert (inc x a). lapply (H1 x y). ir. cluc. am. am. assert (inc y a). lapply (H2 x y). ir; cluc; am. am. ufi property H; ee. ap H7. am. am. rwi leq_create_all H3; xe. rwi leq_create_all H4; xe. assert (inc x a). lapply (H1 x y); ir. cluc; am. am. assert (inc y a). lapply (H2 x y). ir. cluc; am. am. assert (inc z a). lapply (H2 y z); ir. cluc; am. am. ufi property H; ee. ap leq_create_if. am. am. apply H10 with y. am. am. am. rwi leq_create_all H4; xe. rwi leq_create_all H5; xe. Qed.
imports: universe