proposition: Lemma lem2 : forall (p : EP) (y : E), axioms p -> p y -> inc y (create p).
proof: Proof. ir. unfold create in |- *. unfold axioms in H. pose (choose_pr H). set (K := choose (property p)) in *. unfold property in (type of p0). pose (p0 y); xd. Qed.
imports: set_theory