proposition: Theorem not_all_ex_not_proof : forall A (B : A -> Prop), ~(forall x, B x) -> exists x, ~B x.
proof: Proof. intros A B H. apply Classical_Prop.NNPP. intros Habs. elim H. intro x. apply Classical_Prop.NNPP. intro. elim Habs. now exists x. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping