mise sous CVS

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

1 files changed, 20 insertions, 0 deletions

diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
new file mode 100755
index 000000000..a713c0409
--- /dev/null
+++ b/theories/Bool/DecBool.v
@@ -0,0 +1,20 @@
+
+(* $Id$ *)
+
+Implicit Arguments On.
+
+Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
+   := [A,B,C,H,x,y]if H then [_]x else [_]y.
+
+
+Theorem ifdec_left : (A,B:Prop)(C:Set)(H:{A}+{B})~B->(x,y:C)(ifdec H x y)=x.
+Intros; Case H; Auto.
+Intro; Absurd B; Trivial.
+Save.
+
+Theorem ifdec_right : (A,B:Prop)(C:Set)(H:{A}+{B})~A->(x,y:C)(ifdec H x y)=y.
+Intros; Case H; Auto.
+Intro; Absurd A; Trivial.
+Save.
+
+Implicit Arguments Off.