Skip to content

Instantly share code, notes, and snippets.

@nkaretnikov

nkaretnikov/not_exists_dist.v

Created April 27, 2015 00:41
Show Gist options
  • Save nkaretnikov/808fdd7c446fb834558b to your computer and use it in GitHub Desktop.
Save nkaretnikov/808fdd7c446fb834558b to your computer and use it in GitHub Desktop.
Download ZIP
not_exists_dist
Raw
not_exists_dist.v
Theorem not_exists_dist :
excluded_middle ->
forall (X:Type) (P : X -> Prop),
~ (exists x, ~ P x) -> (forall x, P x).
Proof.
intros.
unfold excluded_middle in H.
unfold "~" in H0.
unfold "~" in H.
(* 1 subgoals, subgoal 1 (ID 72) *)
(* H : forall P : Prop, P \/ (P -> False) *)
(* X : Type *)
(* P : X -> Prop *)
(* H0 : (exists x : X, P x -> False) -> False *)
(* x : X *)
(* ============================ *)
(* P x *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment