diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/let-poly.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/let-poly.rkt
index 7bc2ab6fa5..88c39fe4a8 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/let-poly.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/let-poly.rkt
@@ -339,6 +339,21 @@ Capture avoiding substitution
   [(subst M x M_z)
    M])
 
+(define-metafunction stlc
+  [(replace x x x_new)
+   x_new]
+  [(replace (λ x_0 M) x x_new)
+   (λ (replace x_0 x x_new) (replace M x x_new))]
+  [(replace (let ([x_0 M]) N) x x_new)
+   (let ([(replace x_0 x x_new)
+          (replace M x x_new)])
+     (replace N x x_new))]
+  [(replace (M N) x x_new)
+   ((replace M x x_new) (replace N x x_new))]
+  [(replace M x x_new)
+   M])
+
+#;
 (define-metafunction stlc
   [(replace (any_1 ...) x_1 x_new)
    ((replace any_1 x_1 x_new) ...)]
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/jdg-gen.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/jdg-gen.rkt
index b9b58daf19..b96101f323 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/jdg-gen.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/jdg-gen.rkt
@@ -7,6 +7,7 @@
          (only-in "reduction-semantics.rkt"
                   do-test-match)
          "pat-unify.rkt"
+         (only-in "fresh.rkt" variable-not-in)
          (for-syntax racket/base))
 
 (provide pat->term
@@ -20,6 +21,7 @@
 
 ;; pat->term lang pat* env env -> term
 (define (pat->term lang pat full-env [term-e (make-hash)])
+  (displayln (list 'pat->term lang pat))
   (define nt-matchers (make-hash))
   (define eqs (env-eqs full-env))
   (define (get-matcher nt)
@@ -42,6 +44,8 @@
            `(,@(for/list ([p ps]) (recur p)))]
           [`(cstr (,nts ...) ,p)
            (recur p)]
+         [`(variable-not-in ,not-in-p ,sym)
+          (recur not-in-p)]
           [`(nt ,_)
            (okk (ok))]
           [(? predef-pat? _)
@@ -87,6 +91,8 @@
                       (let ([res (recur p)])
                         (unless (not-failed? res) (fail (unif-fail)))
                         res))))]
+        [`(variable-not-in ,not-in-p ,sym)
+         (variable-not-in (recur not-in-p) sym)]
         [_
          (make-term p lang)])))
   (and/fail 
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
index bf88b8af0b..7b8567a298 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
@@ -1492,6 +1492,9 @@
      (and (identifier? #'in-hole)
           (eq? (syntax-e #'in-hole) 'in-hole))
      #''(in-hole . rest)]
+    ;; TODO check that s is quoted or a term
+    [(undatum (variable-not-in (term . tr) . s))
+     #f]
     [(undatum . rest)
      (and (identifier? #'undatum)
           (eq? (syntax-e #'undatum) 'undatum))
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
index fce052f819..c308a21383 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
@@ -414,6 +414,12 @@
                   (if (not-failed? res)
                       res
                       (fail (unif-fail))))))]
+    [`(variable-not-in ,p ,s)
+     (define pat (bind-names p e L))
+     (and/fail (not-failed? pat)
+               (let ([s-pat (bind-names s e L)])
+                 (and/fail (not-failed? s-pat)
+                           `(variable-not-in ,pat ,s-pat))))]
     [`(mismatch-name ,name ,p)
      (define b-pat (bind-names p e L))
      (and/fail (not-failed? b-pat)
@@ -426,51 +432,52 @@
   (define t (resolve t0 e))
   (define u (resolve u0 e))
   #2dmatch
-  ╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═════════════════╦═════════╦══════════╦══════════════╦═════════════╗
-  ║            u    ║ `(mismatch-name ║ `(name      ║ `(cstr        ║`(nt ,n-u) ║`any  ║ (? num-ty?)║`(list        ║ (? pvar?)       ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║
-  ║                 ║   ,u-name       ║   ,name-u   ║   (,nts1 ...) ║           ║      ║            ║  ,us ...)    ║                 ║         ║          ║              ║             ║
-  ║  t              ║   ,u-pat)       ║   ,(bound)) ║   ,p1)        ║           ║      ║            ║              ║                 ║         ║          ║              ║             ║
-  ╠═════════════════╬═════════════════╩═════════════╩═══════════════╩═══════════╩══════╩════════════╩══════════════╩═════════════════╩═════════╩══════════╩══════════════╩═════════════╣
-  ║`(mismatch-name  ║ (hash-set! (dqs-found) t-name (cons u (hash-ref (dqs-found) t-name (λ () '()))))                                                                                 ║
-  ║  ,t-name        ║ (unify* t-pat u e L)                                                                                                                                             ║
-  ║  ,t-pat)        ║                                                                                                                                                                  ║
-  ╠═════════════════╬═════════════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣
-  ║`(name ,name-t   ║                 ║ (instantiate* name-t u e L)                                                                                                                    ║
-  ║       ,(bound)) ║                 ║                                                                                                                                                ║
-  ╠═════════════════╣                 ╚═════════════╦═══════════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣
-  ║`(cstr           ║                               ║(u*-2cstrs     ║ (u*-1cstr nts2 p2 u e L)                                                                                         ║
-  ║  (,nts2 ...)    ║                               ║  nts1 p1      ║                                                                                                                  ║
-  ║  ,p2)           ║                               ║  nts2 p2 e L) ║                                                                                                                  ║
-  ╠═════════════════╣                               ╚═══════════════╬═══════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════╣
-  ║ `(nt ,n-t)      ║                                               ║(u*-2nts   ║ (u*-1nt n-t u e L)                                                                                   ║
-  ║                 ║                                               ║ n-t n-u   ║                                                                                                      ║
-  ║                 ║                                               ║ e L)      ║                                                                                                      ║
-  ╠═════════════════╣                                               ╚═══════════╬══════════════════════════════════════════════════════════════════════════════════════════════════════╣
-  ║  `any           ║                                                           ║ u                                                                                                    ║
-  ║                 ║                                                           ║                                                                                                      ║
-  ╠═════════════════╣                                                           ╚══════╦════════════╦════════════════════════════════════════════════════════════════════╦═════════════╣
-  ║  (? num-ty?)    ║                                                                  ║(u*-2nums   ║                                                                    ║             ║
-  ║                 ║                                                                  ║  t u)      ║                                                                    ║             ║
-  ╠═════════════════╣                                                                  ╚════════════╬══════════════╗                                                     ║             ║
-  ║ `(list ,ts ...) ║                                                                               ║(u*-2lsts     ║                              (unif-fail)            ║             ║
-  ║                 ║                                                                               ║ ts us e L)   ║                                                     ║(u*-matches? ║
-  ╠═════════════════╣                                                                               ╚══════════════╬═════════════════╗                                   ║  t u        ║
-  ║ (? pvar?)       ║                                                                                              ║(u*-2pvars u t L)║                                   ║  e L)       ║
-  ╠═════════════════╣                                                                                              ╚═════════════════╬═════════╗                         ║             ║
-  ║ `string         ║                   (unify* u t e L)                                                                             ║    t    ║                         ║             ║
-  ╠═════════════════╣                                                                                                                ╚═════════╬══════════╗              ║             ║
-  ║ `boolean        ║                                                                                                                          ║    t     ║              ║             ║
-  ╠═════════════════╣                                                                                                                          ╚══════════╬══════════════╣             ║
-  ║ (? base-ty?)    ║                                                                                                                                     ║      t       ║             ║
-  ╠═════════════════╣                                                                                                                                     ╚══════════════╬═════════════╣
-  ║ (? not-pair?)   ║                                                                                                                                                    ║(and/fail    ║
-  ║                 ║                                                                                                                                                    ║ (equal? t u)║
-  ║                 ║                                                                                                                                                    ║ t)          ║
-  ╚═════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝)
+  ╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═══════════════════╦═════════╦══════════╦══════════════╦═════════════╗
+  ║            u    ║ `(mismatch-name ║ `(name      ║ `(cstr        ║`(nt ,n-u) ║`any  ║ (? num-ty?)║`(list        ║ (? pvar?)         ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║
+  ║                 ║   ,u-name       ║   ,name-u   ║   (,nts1 ...) ║           ║      ║            ║  ,us ...)    ║                   ║         ║          ║              ║             ║
+  ║  t              ║   ,u-pat)       ║   ,(bound)) ║   ,p1)        ║           ║      ║            ║              ║                   ║         ║          ║              ║             ║
+  ╠═════════════════╬═════════════════╩═════════════╩═══════════════╩═══════════╩══════╩════════════╩══════════════╩═══════════════════╩═════════╩══════════╩══════════════╩═════════════╣
+  ║`(mismatch-name  ║ (hash-set! (dqs-found) t-name (cons u (hash-ref (dqs-found) t-name (λ () '()))))                                                                                   ║
+  ║  ,t-name        ║ (unify* t-pat u e L)                                                                                                                                               ║
+  ║  ,t-pat)        ║                                                                                                                                                                    ║
+  ╠═════════════════╬═════════════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣
+  ║`(name ,name-t   ║                 ║ (instantiate* name-t u e L)                                                                                                                      ║
+  ║       ,(bound)) ║                 ║                                                                                                                                                  ║
+  ╠═════════════════╣                 ╚═════════════╦═══════════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣
+  ║`(cstr           ║                               ║(u*-2cstrs     ║ (u*-1cstr nts2 p2 u e L)                                                                                           ║
+  ║  (,nts2 ...)    ║                               ║  nts1 p1      ║                                                                                                                    ║
+  ║  ,p2)           ║                               ║  nts2 p2 e L) ║                                                                                                                    ║
+  ╠═════════════════╣                               ╚═══════════════╬═══════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════╣
+  ║ `(nt ,n-t)      ║                                               ║(u*-2nts   ║ (u*-1nt n-t u e L)                                                                                     ║
+  ║                 ║                                               ║ n-t n-u   ║                                                                                                        ║
+  ║                 ║                                               ║ e L)      ║                                                                                                        ║
+  ╠═════════════════╣                                               ╚═══════════╬════════════════════════════════════════════════════════════════════════════════════════════════════════╣
+  ║  `any           ║                                                           ║ u                                                                                                      ║
+  ║                 ║                                                           ║                                                                                                        ║
+  ╠═════════════════╣                                                           ╚══════╦════════════╦══════════════════════════════════════════════════════════════════════╦═════════════╣
+  ║  (? num-ty?)    ║                                                                  ║(u*-2nums   ║                                                                      ║             ║
+  ║                 ║                                                                  ║  t u)      ║                                                                      ║             ║
+  ╠═════════════════╣                                                                  ╚════════════╬══════════════╗                                                       ║             ║
+  ║ `(list ,ts ...) ║                                                                               ║(u*-2lsts     ║                                (unif-fail)            ║             ║
+  ║                 ║                                                                               ║ ts us e L)   ║                                                       ║(u*-matches? ║
+  ╠═════════════════╣                                                                               ╚══════════════╬═══════════════════╗                                   ║  t u        ║
+  ║ (? pvar?)       ║                                                                                              ║(u*-2pvars u t e L)║                                   ║  e L)       ║
+  ╠═════════════════╣                                                                                              ╚═══════════════════╬═════════╗                         ║             ║
+  ║ `string         ║                   (unify* u t e L)                                                                               ║    t    ║                         ║             ║
+  ╠═════════════════╣                                                                                                                  ╚═════════╬══════════╗              ║             ║
+  ║ `boolean        ║                                                                                                                            ║    t     ║              ║             ║
+  ╠═════════════════╣                                                                                                                            ╚══════════╬══════════════╣             ║
+  ║ (? base-ty?)    ║                                                                                                                                       ║      t       ║             ║
+  ╠═════════════════╣                                                                                                                                       ╚══════════════╬═════════════╣
+  ║ (? not-pair?)   ║                                                                                                                                                      ║(and/fail    ║
+  ║                 ║                                                                                                                                                      ║ (equal? t u)║
+  ║                 ║                                                                                                                                                      ║ t)          ║
+  ╚═════════════════╩══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝)
 
 (define (pvar? x) (or (vnom? x)
                       (var-pref? x)
                       (var-exc? x)
+                      (vni? x)
                       (equal? 'variable x)))
 (define (vnom? x) (equal? x 'variable-not-otherwise-mentioned))
 (define (var-pref? x) (match x
@@ -480,33 +487,56 @@
                        [`(variable-except ,p ...) #t]
                        [_ #f]))
 (define (not-pair? x) (not (pair? x)))
+(define vni?
+  (match-lambda [`(variable-not-in ,e ,s) #t]
+                [_ #f]))
 
-(define (u*-2pvars v1 v2 L)
+(define (u*-2pvars v1 v2 e L)
   #2dmatch
-  ╔════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╗
-  ║                   v1   ║`(variable-prefix ,p1)    ║ `(variable-except ,e1 ... )    ║    (? vnom?)                  ║   `variable    ║
-  ║ v2                     ║                          ║                                ║                               ║                ║
-  ╠════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╣
-  ║                        ║ (cond                    ║ (and/fail                      ║(u*-2pvars                     ║                ║
-  ║ `(variable-prefix ,p2) ║  [(sym-pref? p1 p2)      ║  (not (ormap                   ║ v2                            ║                ║
-  ║                        ║   `(variable-prefix ,p2)]║        (curry sym-pref? p2)    ║ `(variable-except             ║                ║
-  ║                        ║  [(sym-pref? p2 p1)      ║        e1))                    ║ ,@(compiled-lang-literals L)) ║                ║
-  ║                        ║   `(variable-prefix ,p1)]║  v2)                           ║ L)                            ║                ║
-  ║                        ║  [else (unif-fail)])     ║                                ║                               ║                ║
-  ╠════════════════════════╬══════════════════════════╬════════════════════════════════╣                               ║                ║
-  ║                        ║                          ║ `(variable-except              ║                               ║                ║
-  ║  `(variable-except     ║                          ║   ,@(de-dupe/sorted            ║                               ║       v2       ║
-  ║     ,e2 ...)           ║                          ║      (merge/sorted e1 e2)))    ║                               ║                ║
-  ║                        ║                          ║                                ║                               ║                ║
-  ╠════════════════════════╣                          ╚════════════════════════════════╬═══════════════════════════════╣                ║
-  ║                        ║                                                           ║                               ║                ║
-  ║  (? vnom?)             ║                                                           ║              v1               ║                ║
-  ║                        ║                                                           ║                               ║                ║
-  ╠════════════════════════╣               (u*-2pvars v2 v1 L)                         ╚═══════════════════════════════╣                ║
-  ║                        ║                                                                                           ║                ║
-  ║ `variable              ║                                                                                           ║                ║
-  ║                        ║                                                                                           ║                ║
-  ╚════════════════════════╩═══════════════════════════════════════════════════════════════════════════════════════════╩════════════════╝)
+  ╔══════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╦══════════════════════════════════════╗
+  ║                   v1     ║`(variable-prefix ,p1)    ║ `(variable-except ,e1 ... )    ║    (? vnom?)                  ║   `variable    ║`(variable-not-in ,e1 ,s)             ║       
+  ║ v2                       ║                          ║                                ║                               ║                ║                                      ║
+  ╠══════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╬══════════════════════════════════════╣
+  ║                          ║ (cond                    ║ (and/fail                      ║(u*-2pvars                     ║                ║(and/fail                             ║
+  ║ `(variable-prefix ,p2)   ║  [(sym-pref? p1 p2)      ║  (not (ormap                   ║ v2                            ║                ║  (sym-pref? p2 s)                    ║
+  ║                          ║   `(variable-prefix ,p2)]║        (curry sym-pref? p2)    ║ `(variable-except             ║                ║  v1)                                 ║
+  ║                          ║  [(sym-pref? p2 p1)      ║        e1))                    ║ ,@(compiled-lang-literals L)) ║                ║                                      ║
+  ║                          ║   `(variable-prefix ,p1)]║  v2)                           ║ e L)                          ║                ║                                      ║
+  ║                          ║  [else (unif-fail)])     ║                                ║                               ║                ║                                      ║
+  ╠══════════════════════════╬══════════════════════════╬════════════════════════════════╣                               ║                ╠══════════════════════════════════════╣
+  ║                          ║                          ║ `(variable-except              ║                               ║                ║`(variable-not-in                     ║
+  ║  `(variable-except       ║                          ║   ,@(de-dupe/sorted            ║                               ║       v2       ║   (list ,e1 ,@e2)                    ║
+  ║     ,e2 ...)             ║                          ║      (merge/sorted e1 e2)))    ║                               ║                ║   ,s)                                ║
+  ║                          ║                          ║                                ║                               ║                ║                                      ║
+  ╠══════════════════════════╣                          ╚════════════════════════════════╬═══════════════════════════════╣                ╠══════════════════════════════════════╣
+  ║                          ║                                                           ║                               ║                ║(u*-2pvars v1                         ║
+  ║  (? vnom?)               ║                                                           ║              v1               ║                ║`(variable-except                     ║
+  ║                          ║                                                           ║                               ║                ║  ,@(compiled-lang-literals L))       ║
+  ║                          ║                                                           ║                               ║                ║ e L)                                 ║
+  ╠══════════════════════════╣               (u*-2pvars v2 v1 e L)                       ╚═══════════════════════════════╣                ╠══════════════════════════════════════╣
+  ║                          ║                                                                                           ║                ║                                      ║
+  ║ `variable                ║                                                                                           ║                ║              v1                      ║  
+  ║                          ║                                                                                           ║                ║                                      ║
+  ╠══════════════════════════╣                                                                                           ╚════════════════╬══════════════════════════════════════╣
+  ║                          ║                                                                                                            ║                                      ║
+  ║ `(variable-not-in ,e2 ,t)║                                                                                                            ║     (2-vnis v1 v2 e L)               ║  
+  ║                          ║                                                                                                            ║                                      ║
+  ╚══════════════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════╩══════════════════════════════════════╝)
+
+(define (2-vnis v1 v2 e L)
+  (match-define `(variable-not-in ,e1 ,s1) v1)
+  (match-define `(variable-not-in ,e2 ,s2) v2)
+  (cond
+    [(not (and (symbol? s1) (symbol? s2)))
+     (displayln (list s1 s2))
+     (define s-res (unify* s1 s2 e L))
+     (and/fail s-res
+               `(variable-not-in (list ,e1 ,e2) ,s-res))]
+    [(sym-pref? s1 s2)
+     `(variable-not-in (list ,e1 ,e2) s2)]
+    [(sym-pref? s2 s1)
+     `(variable-not-in (list ,e1 ,e2) s1)]
+    [else (unif-fail)]))
 
 (define (sym-pref? sp s)
   (regexp-match
@@ -780,24 +810,25 @@
     [_
      (values (lvar id) res)]))
 
-(provide check-nt)
+(provide check-nt
+         normalize-pat)
 
 (define check-nt
   (let ([memo (hash)])
     (λ (nt clang pat)
-      (define npat (normalize-pat pat))
+      (define npat (normalize-pat clang pat))
       (hash-ref memo (list nt clang npat)
                 (λ ()
                   (define pat-ok? 
-                    (for/or ([ntp (in-list (map normalize-pat (nt-pats nt clang)))])
+                    (for/or ([ntp (in-list (map ((curry normalize-pat) clang) (nt-pats nt clang)))])
                       (not-failed? (unify* npat ntp #f empty-lang))))
                   (set! memo
                         (hash-set memo (list nt clang npat) pat-ok?))
                   pat-ok?)))))
 
-(define (normalize-pat pat)
+(define (normalize-pat lang pat)
   (let loop ([pat pat])
-    (match-a-pattern pat
+    (match-a-pattern #:allow-else pat
                      [`any pat]
                      [`number pat]
                      [`string pat]
@@ -809,27 +840,34 @@
                      [`(variable-except ,s ...) `variable]
                      [`(variable-prefix ,s) `variable]
                      [`variable-not-otherwise-mentioned pat]
-                     [`hole (error "can't normalize pattern: ~s" pat)]
-                     [`(nt ,id) `any]
+                     [`hole (error 'normalize-pat "can't normalize pattern: ~s" pat)]
+                     [`(nt ,id)
+                      (loop (hash-ref (compiled-lang-collapsible-nts lang) id 'any))]
                      [`(name ,name ,npat)
                       (if (bound? npat)
                           `any
                           `(name ,name ,(loop npat)))]
                      [`(mismatch-name ,name ,pat) (loop pat)]
-                     [`(in-hole ,p1 ,p2) (error "can't normalize pattern: ~s" pat)]
+                     [`(in-hole ,p1 ,p2) (error 'normalize-pat "can't normalize pattern: ~s" pat)]
                      [`(hide-hole ,p) (loop p)]
                      [`(side-condition ,p ,g ,e)
-                      (error "can't normalize pattern: ~s" pat)]
-                     [`(cross ,s) (error "can't normalize pattern: ~s" pat)]
+                      (error 'normalize-pat "can't normalize pattern: ~s" pat)]
+                     [`(cross ,s) (error 'normalize-pat "can't normalize pattern: ~s" pat)]
                      [`(list ,sub-pats ...)
                       `(list ,@(for/list ([sub-pat (in-list sub-pats)])
                                  (match sub-pat
                                    [`(repeat ,pat ,name ,mismatch)
-                                    (error "can't normalize pattern: ~s" pat)]
+                                    (error 'normalize-pat "can't normalize pattern: ~s" sub-pat)]
                                    [_
                                     (loop sub-pat)])))]
                      [(? (compose not pair?)) 
-                      pat])))
+                      pat]
+                     [_
+                      (match pat
+                        [`(variable-not-in ,p ,s)
+                         `variable])])))
+
+(provide nt-pats)
 
 (define (nt-pats nt lang)
   (define this-rhs
@@ -868,6 +906,8 @@
      `(name ,new-id ,(fresh-pat-vars pat instantiations))]
     [`(list ,pats ...)
      `(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))]
+    [`(variable-not-in ,pat ,s)
+     `(variable-not-in ,(fresh-pat-vars pat instantiations) ,s)]
     [_ pre-pat]))
 
 (define (make-uid id)
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt
index 915e62b925..f5b753f251 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt
@@ -69,14 +69,14 @@
   (define name-nums 0)
   (define fresh-pat (parameterize ([unique-name-nums 0])
                       (begin0
-                       (fresh-pat-vars input (make-hash))
-                       (set! name-nums (unique-name-nums)))))
+                        (fresh-pat-vars input (make-hash))
+                        (set! name-nums (unique-name-nums)))))
   (define fs (list (fail-cont empty-env
-                             (list (make-partial-rule fresh-pat (if (shuffle-clauses?)
-                                                                    (shuffle clauses)
-                                                                    (order-clauses clauses))
-                                                      '() bound))
-                             bound)))
+                              (list (make-partial-rule fresh-pat (if (shuffle-clauses?)
+                                                                     (shuffle clauses)
+                                                                     (order-clauses clauses))
+                                                       '() bound))
+                              bound)))
   (define v-locs (make-hash))
   (λ ()
     (parameterize ([unique-name-nums name-nums]
@@ -93,11 +93,12 @@
           (values (and/fail env/f (unify fresh-pat 'any env/f lang))
                   fails)))
       (set-last-gen-trace! (generation-trace))
-      (when (success-jump?)
-        (set! fs (shuffle-fails fails)))  ;; how to test if we're randomizing here?
+      (set! fs (if (success-jump?)
+                   fails
+                   (shuffle-fails fails)))  ;; how to test if we're randomizing here?
       (set! name-nums (unique-name-nums))
       ans)))
-  
+
 (define (trim-fails fs)
   (define rev-fs (reverse fs))
   (reverse
@@ -131,44 +132,43 @@
 
 (define (push-down a-partial-rule env fringe fail)
   (inc-pushdown-count)
-  (match a-partial-rule
-    [(partial-rule pat clauses tr-loc bound)
-     (check-depth-limits bound tr-loc fail)
+  (match-define (partial-rule pat clauses tr-loc bound) a-partial-rule)
+  (check-depth-limits bound tr-loc fail)
+  (cond
+    [(null? clauses)
+     (fail-back fail)]
+    [else
+     (define the-clause (fresh-clause-vars (car clauses)))
+     (define res-pe (do-unification the-clause pat env))
+     (when (log-receiver? gen-log-recv)
+       (log-message (current-logger) 'info (symbol->string (clause-name the-clause))
+                    (gen-trace tr-loc the-clause pat (and res-pe #t) bound env)))
+     (define failure-fringe
+       (cons (struct-copy partial-rule
+                          a-partial-rule
+                          [clauses (cdr clauses)])
+             fringe))
      (cond
-       [(null? clauses)
-        (fail-back fail)]
+       [(not res-pe)
+        (choose-rule env failure-fringe fail)]
        [else
-        (define the-clause (fresh-clause-vars (car clauses)))
-        (define res-pe (do-unification the-clause pat env))
-        (when (log-receiver? gen-log-recv)
-          (log-message (current-logger) 'info (symbol->string (clause-name the-clause))
-                       (gen-trace tr-loc the-clause pat (and res-pe #t) bound env)))
-        (define failure-fringe
-          (cons (struct-copy partial-rule
-                             a-partial-rule
-                             [clauses (cdr clauses)])
-                fringe))
-        (cond
-          [(not res-pe)
-           (choose-rule env failure-fringe fail)]
-          [else
-           (define new-fringe-elements
-             (for/list ([prem (in-list (clause-prems the-clause))]
-                        [n (in-naturals)])
-               (define prem-cls (prem-clauses prem))
-               (make-partial-rule (prem-pat prem) 
-                                  (if (positive? bound)
-                                      (if (shuffle-clauses?)
-                                          (shuffle prem-cls)
-                                          (order-clauses prem-cls))
-                                      (order-clauses prem-cls))
-                                  (cons n tr-loc)
-                                  (- bound 1))))
-           (define new-fringe (append new-fringe-elements
-                                      fringe))
-           (choose-rule (p*e-e res-pe)
-                        new-fringe
-                        (cons (fail-cont env failure-fringe bound) fail))])])]))
+        (define new-fringe-elements
+          (for/list ([prem (in-list (clause-prems the-clause))]
+                     [n (in-naturals)])
+            (define prem-cls (prem-clauses prem))
+            (make-partial-rule (prem-pat prem) 
+                               (if (positive? bound)
+                                   (if (shuffle-clauses?)
+                                       (shuffle prem-cls)
+                                       (order-clauses prem-cls))
+                                   (order-clauses prem-cls))
+                               (cons n tr-loc)
+                               (- bound 1))))
+        (define new-fringe (append new-fringe-elements
+                                   fringe))
+        (choose-rule (p*e-e res-pe)
+                     new-fringe
+                     (cons (fail-cont env failure-fringe bound) fail))])]))
 
 (define (order-clauses cs)
   (define num-prems->cs (hash))
@@ -184,37 +184,36 @@
   (apply append
          (for/list ([k (sort (hash-keys num-prems->cs) <)])
            (shuffle (set->list (hash-ref num-prems->cs k))))))
-  
+
 
 
 (define (do-unification clse input env)
-  (match clse
-    [(clause head-pat eq/dqs prems lang name)
-     (define-values (eqs dqs) (partition eqn? eq/dqs))
-     (define env1
-       (let loop ([e env]
-                  [dqs dqs])
-         (match dqs
-           ['() e]
-           [(cons (dqn ps lhs rhs) rest)
-            (dqn ps lhs rhs)
-            (define u-res (disunify ps lhs rhs e lang))
-            (and u-res
-                 (loop u-res rest))])))
-     (define head-p*e (and/fail env1 (unify input head-pat env1 lang)))
-     (cond
-       [(not-failed? head-p*e)
-        (define res-p (p*e-p head-p*e))
-        (let loop ([e (p*e-e head-p*e)]
-                   [eqs eqs])
-          (match eqs
-            ['() 
-             (p*e (p*e-p head-p*e) e)]
-            [(cons (eqn lhs rhs) rest)
-             (define u-res (unify lhs rhs e lang))
-             (and (not-failed? u-res)
-                  (loop (p*e-e u-res) rest))]))]
-       [else #f])]))
+  (match-define (clause head-pat eq/dqs prems lang name) clse)
+  (clause head-pat eq/dqs prems lang name)
+  (define-values (eqs dqs) (partition eqn? eq/dqs))
+  (define env1
+    (let loop ([e env]
+               [dqs dqs])
+      (match dqs
+        ['() e]
+        [(cons (dqn ps lhs rhs) rest)
+         (define u-res (disunify ps lhs rhs e lang))
+         (and u-res
+              (loop u-res rest))])))
+  (define head-p*e (and/fail env1 (unify input head-pat env1 lang)))
+  (cond
+    [(not-failed? head-p*e)
+     (define res-p (p*e-p head-p*e))
+     (let loop ([e (p*e-e head-p*e)]
+                [eqs eqs])
+       (match eqs
+         ['() 
+          (p*e (p*e-p head-p*e) e)]
+         [(cons (eqn lhs rhs) rest)
+          (define u-res (unify lhs rhs e lang))
+          (and (not-failed? u-res)
+               (loop (p*e-e u-res) rest))]))]
+    [else #f]))
 
 (define (fresh-clause-vars clause-raw)
   (define instantiations (make-hash))
@@ -227,10 +226,10 @@
                                  (fresh-pat-vars rhs instantiations))]
                            [(dqn ps lhs rhs)
                             (dqn (map (λ (id) (hash-ref instantiations id
-                                                       (λ () 
-                                                         (define unique-id (make-uid id))
-                                                         (hash-set! instantiations id unique-id)
-                                                         unique-id)))
+                                                        (λ () 
+                                                          (define unique-id (make-uid id))
+                                                          (hash-set! instantiations id unique-id)
+                                                          unique-id)))
                                       ps)
                                  (fresh-pat-vars lhs instantiations)
                                  (fresh-pat-vars rhs instantiations))]))]
@@ -244,13 +243,15 @@
 (define (check-depth-limits bound tr-loc fails)
   (when ((pushdown-count) . > . (pushdown-limit))
     (define str (format "pushdown count of ~s exceeded at ~s" (pushdown-count) tr-loc))
-    ;(printf "!*\n\t~s\t*!\n" str)
+    (printf "!*\n\t~s\t*!\n" str)
     (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
   (when (> (bt-count) (bt-limit))
     (define str (format "backtrack count of ~s exceeded at ~s" (bt-limit) tr-loc))
+    (displayln str)
     (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
   (when (> (length tr-loc) (* 3 (+ (length tr-loc) bound)))
     (define str (format "depth bound exceeded at depth: ~s" (length tr-loc)))
+    (displayln str)
     (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))))
 
 
diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
index a8a119edde..ebbb98bc57 100644
--- a/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
+++ b/pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
@@ -8,6 +8,7 @@
                      (only-in racket/list flatten)
                      "keyword-macros.rkt"
                      "matcher.rkt")
+         (only-in "fresh.rkt" variable-not-in)
          syntax/datum
          "error.rkt"
          "lang-struct.rkt"
@@ -330,9 +331,16 @@
      (d->pat #'d names)]))
 
 (define-for-syntax (d->pat d names)
-  (syntax-case d (... undatum in-hole undatum-splicing)
+  (syntax-case d (... undatum in-hole undatum-splicing variable-not-in term quote)
     [()
      #'(list)]
+    [(undatum (variable-not-in (term t) (quote s)))
+     (with-syntax ([t-pat (d->pat #'t names)])
+       #'(variable-not-in t-pat s))]
+    [(undatum (variable-not-in (term t1) (term t2)))
+     (with-syntax ([t1-pat (d->pat #'t1 names)]
+                   [t2-pat (d->pat #'t2 names)])
+       #'(variable-not-in t1-pat t2-pat))]
     [(undatum rest ...) ;; holes are also undatumed
      d]
     [(undatum-splicing rest ...)