proposition: Lemma not_forall_imply_exists_not : forall A (P : A -> Prop), ~(forall x, P x) -> exists x, ~P x.
proof: Proof. intros. apply NNPP. intro. apply H. intros. elim (classic (P x)). auto. intro. absurd (exists x, ~ P x). exact H0. exists x. exact H1. Qed.
imports: CoLoR(LogicUtil)