Ajout 'exists! x:A, P

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

1 files changed, 9 insertions, 0 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index cefbb989de..f50e796827 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -141,6 +141,15 @@ Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
    format "'[' 'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
+Notation "'exists' ! x , P" := 
+  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
+Notation "'exists' ! x : A , P" := 
+  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
+
 
 (** Derived rules for universal quantification *)