diff --git a/collects/racket/contract.rkt b/collects/racket/contract.rkt
index 5b660bd6c0..896b8ae338 100644
--- a/collects/racket/contract.rkt
+++ b/collects/racket/contract.rkt
@@ -16,7 +16,7 @@ differences from v3:
          "private/define-struct.rkt")
 
 (provide (all-from-out "contract/base.rkt")
- (except-out (all-from-out racket/contract/exists) ∃?)
+ (except-out (all-from-out racket/contract/exists) ∀∃?)
  (all-from-out racket/contract/regions))
 
 ;; ======================================================================
diff --git a/collects/racket/contract/exists.rkt b/collects/racket/contract/exists.rkt
index e2896253eb..94f15e80b6 100644
--- a/collects/racket/contract/exists.rkt
+++ b/collects/racket/contract/exists.rkt
@@ -3,14 +3,16 @@
 (require "private/guts.rkt")
 
 (provide new-∃/c
-         ∃?)
+         new-∀/c
+         ∀∃?)
 
-(define (∃-proj ctc)
-  (let ([in (∃/c-in ctc)]
-        [out (∃/c-out ctc)]
-        [pred? (∃/c-pred? ctc)])
+(define (∀∃-proj ctc)
+  (let ([in (∀∃/c-in ctc)]
+        [out (∀∃/c-out ctc)]
+        [pred? (∀∃/c-pred? ctc)]
+        [neg? (∀∃/c-neg? ctc)])
   (λ (blame)
-    (if (blame-swapped? blame)
+    (if (eq? neg? (blame-swapped? blame))
         (λ (val)
           (if (pred? val)
               (out val)
@@ -20,18 +22,22 @@
                                  val)))
 	in))))
 
-(define-struct ∃/c (in out pred? name)
+(define-struct ∀∃/c (in out pred? name neg?)
   #:omit-define-syntaxes
   #:property prop:contract
   (build-contract-property
-   #:name (λ (ctc) (∃/c-name ctc))
+   #:name (λ (ctc) (∀∃/c-name ctc))
    #:first-order (λ (ctc) (λ (x) #t)) ;; ???
-   #:projection ∃-proj))
+   #:projection ∀∃-proj))
 
-(define-struct ∃ ())
+(define-struct ∀∃ ())
 
-(define (new-∃/c raw-name)
-  (define name (string->symbol (format "~a/∃" raw-name)))
+(define (new-∃/c raw-name) (mk raw-name #t))
+(define (new-∀/c raw-name) (mk raw-name #f))
+
+(define (mk raw-name neg?)
+  (define name (string->symbol (format "~a/~a" raw-name (if neg? "∃" "∀"))))
   (define-values (struct-type constructor predicate accessor mutator)
-    (make-struct-type name struct:∃ 1 0))
-  (make-∃/c constructor (λ (x) (accessor x 0)) predicate raw-name))
+    (make-struct-type name struct:∀∃ 1 0))
+  (make-∀∃/c constructor (λ (x) (accessor x 0)) predicate raw-name neg?))
+
diff --git a/collects/scheme/exists/lang.rkt b/collects/scheme/exists/lang.rkt
index e750a8d967..443205d8a9 100644
--- a/collects/scheme/exists/lang.rkt
+++ b/collects/scheme/exists/lang.rkt
@@ -243,7 +243,7 @@
     #'(begin
         (define -predicates
           (let ([predicates (λ (x) 
-                              (if (∃? x)
+                              (if (∀∃? x)
                                   (error 'predicates "supplied with a wrapped value ~e" x)
                                   (predicates x)))])
             predicates)) 
diff --git a/collects/scribblings/reference/contracts.scrbl b/collects/scribblings/reference/contracts.scrbl
index 84aad56de7..34b893bade 100644
--- a/collects/scribblings/reference/contracts.scrbl
+++ b/collects/scribblings/reference/contracts.scrbl
@@ -424,15 +424,42 @@ Constructs a contract on a promise. The contract does not force the
 promise, but when the promise is forced, the contract checks that the
 result value meets the contract produced by @racket[expr].}
 
+
+@defproc[(new-∀/c [name symbol?]) contract?]{
+  Constructs a new universal contract. 
+  
+  Universal contracts accept all values when in negative positions (e.g., function
+  inputs) and wrap them in an opaque struct, hiding the precise value. 
+  In positive positions (e.g. function returns), 
+  a universal contract accepts only values that were previously accepted in negative positions (by checking
+  for the wrappers).
+  
+  The name is used to identify the contract in error messages.
+  
+  For example, this contract:
+  @racketblock[(let ([a (new-∃/c 'a)])
+                 (-> a a))]
+  describes the identity function (or a non-terminating function)
+  That is, the first use of the @racket[a] appears in a
+  negative position and thus inputs to that function are wrapped with an opaque struct.
+  Then, when the function returns, it is checked to see if the result is wrapped, since
+  the second @racket[a] appears in a positive position.
+
+  This is a dual to @racket[new-∃/c].
+  
+}
+
 @defproc[(new-∃/c [name symbol?]) contract?]{
   Constructs a new existential contract. 
   
   Existential contracts accept all values when in positive positions (e.g., function
-  returns) and wraps the value in an opaque struct, hiding the precise value. 
+  returns) and wrap them in an opaque struct, hiding the precise value. 
   In negative positions (e.g. function inputs), 
-  it accepts only values that were previously accepted in negative positions (by checking
+  they accepts only values that were previously accepted in positive positions (by checking
   for the wrappers).
   
+  The name is used to identify the contract in error messages.
+  
   For example, this contract:
   @racketblock[(let ([a (new-∃/c 'a)])
                  (-> (-> a a)
@@ -443,8 +470,10 @@ result value meets the contract produced by @racket[expr].}
   Then, when the function returns, it is checked to see if the result is wrapped, since
   the second @racket[a] appears in a negative position.
   
+  This is a dual to @racket[new-∀/c].
 }
 
+
 @; ------------------------------------------------------------------------
 
 @section{Function Contracts}
diff --git a/collects/tests/racket/contract-test.rktl b/collects/tests/racket/contract-test.rktl
index f6746f065b..28e1e98fbc 100644
--- a/collects/tests/racket/contract-test.rktl
+++ b/collects/tests/racket/contract-test.rktl
@@ -9984,6 +9984,31 @@ so that propagation occurs.
        (λ (x) x)))
    11)
   
+  (test/pos-blame
+   '∀1
+   '(contract (new-∀/c 'pair)
+              1
+              'pos
+              'neg))
+  
+  (test/spec-passed
+   '∀2
+   '((contract (-> (new-∀/c 'pair) any/c)
+               (λ (x) x)
+               'pos
+               'neg)
+     1))
+  
+  (test/spec-passed/result
+   '∀3
+   '(let ([pair (new-∀/c 'pair)])
+      ((contract (-> pair pair)
+                 (λ (x) x)
+                 'pos
+                 'neg)
+       11))
+   11)
+  
 ;                                                        
 ;                                                        
 ;