proposition: Lemma not_exists_pr : forall p : EP, ~ ex p <-> (forall x : E, ~ p x).
proof: Proof. ir. unfold iff in |- *. ap conj. ir. unfold not in |- *. unfold not in H. ir. ap H. apply ex_intro with x. am. ir. unfold not in |- *. unfold not in H. ir. nin H0. apply H with x. am. Qed.
imports: tactics