Introduction d'une preuve de False_rec

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1507 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 1 deletions

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index c86c38dd59..1f1ad6ce55 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -14,6 +14,7 @@
 
 Require Export Logic.
 Require LogicSyntax.
+Require Datatypes.
 
 Section Subsets.
 
@@ -166,7 +167,23 @@ Syntactic Definition Value := (value ?).
 (* Self realizing propositions *)
 (*******************************)
 
-Axiom False_rec : (P:Set)False->P.
+(* [False -> C] can be proved for [C:Set] using informative 
+   elimination for equality  
+
+   [Axiom False_rec : (P:Set)False->P.]
+
+*)
+
+Definition Q:=[P:Set][b:bool]if b then unit else P.
+
+Lemma False_rec : (P:Set)False->P.
+Intros.
+Change (Q P false).
+Cut true=false.
+Intro H1; Case H1.
+Exact tt.
+Contradiction.
+Save.
 
 Lemma False_rect: (C:Type)False->C.
 Proof.