proposition: Lemma lem1 : forall (p : EP) (y : E), axioms p -> inc y (create p) -> p y.
proof: Proof. ir. unfold create in H0. unfold axioms in H. pose (choose_pr H). unfold property in H0. unfold property in (type of p0). pose (p0 y). xd. Qed.
imports: set_theory