diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 22:58:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 22:58:23 +0000 |
| commit | 9e95b47304c98e4bc41b6b31bf5ef96aba410851 (patch) | |
| tree | 890ca2d41e84860291bfd91ad67ac37daa029d20 /theories/Logic/ClassicalDescription.v | |
| parent | 1f77a10f41e07324fd3df3676d68e005dd311e1b (diff) | |
Renforcement significatif du resultat principal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ClassicalDescription.v')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 82077696d..144d7d06a 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -44,9 +44,9 @@ Qed. (** The followig proof comes from [1] *) -Theorem classic_set : (P:Prop)({P}+{~P} -> False) -> False. +Theorem classic_set : (((P:Prop){P}+{~P}) -> False) -> False. Proof. -Intros P HnotEM. +Intro HnotEM. Pose R:=[A,b]A/\true=b \/ ~A/\false=b. Assert H:(EX f:Prop->bool|(A:Prop)(R A (f A))). Apply description. @@ -64,6 +64,7 @@ NewDestruct (classic A) as [Ha|Hnota]. Assumption. NewDestruct H as [f Hf]. Apply HnotEM. +Intro P. Assert HfP := (Hf P). (* Elimination from Hf to Set is not allowed but from f to Set yes ! *) NewDestruct (f P). |