From 9a890c748ed55e9b1ccff37b41ddcbfd371cf727 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 May 2010 11:49:15 +0000
Subject: Generalized the formulation of classic_set in propositional contexts
 (consequence of classical unique choice)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13030 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Logic/ClassicalUniqueChoice.v | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 67b853be94..6389e447f3 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -46,9 +46,10 @@ Qed.
 
 Require Import Setoid.
 
-Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Theorem classic_set_in_prop_context :
+  forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-intro HnotEM.
+intros C HnotEM.
 set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
 assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
 apply unique_choice.
@@ -80,3 +81,11 @@ destruct (f P).
     assumption.
 Qed.
 
+Corollary not_not_classic_set :
+  ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Proof.
+apply classic_set_in_prop_context.
+Qed.
+
+(* Compatibility *)
+Notation classic_set := not_not_classic_set (only parsing).
-- 
cgit v1.2.3