diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-diffs.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-diffs.rkt
index 24c2478dcb..38eb38ac59 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-diffs.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-diffs.rkt
@@ -31,4 +31,10 @@
 (module+ main
   (command-line
    #:args ([dir #f])
-   (void (make-diffs dir))))
+   (begin
+     (when dir
+       (unless (member dir directories)
+         (raise-user-error 'make-diffs.rkt 
+                           "expected one of the following directories: ~s" 
+                           directories)))
+     (void (make-diffs dir)))))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-mutants.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-mutants.rkt
index b2fa1395b5..47325e131d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-mutants.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-mutants.rkt
@@ -46,4 +46,10 @@
 (module+ main
   (command-line
    #:args ([dir #f])
-   (void (make-mutants dir))))
+   (begin
+     (when dir
+       (unless (member dir directories)
+         (raise-user-error 'make-mutants.rkt 
+                           "expected one of the following directories: ~s" 
+                           directories)))
+     (void (make-mutants dir)))))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
index 5c153d216a..44da271767 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
@@ -8,11 +8,11 @@
 12a11,12
 > (define the-error "the order of the variable clauses is swapped")
 > 
-104,105d103
+106,107d105
 <   [(subst x x M)
 <    M]
-107a106,107
+109a108,109
 >   [(subst x x M)
 >    M]
-255a256
+257a258
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
deleted file mode 100644
index 3cac19e68f..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
+++ /dev/null
@@ -1,16 +0,0 @@
-3,4d2
-< (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "only substitutes inside of hd constants")
-> 
-114,115c114,115
-<   [(subst (c M) x M_x)
-<    (c (subst M x M_x))]
----
->   [(subst (hd M) x M_x)
->    (hd (subst M x M_x))]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
index fe3b52434f..a98a344fa5 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
@@ -8,9 +8,9 @@
 12a11,12
 > (define the-error "substitutes rator into rand in application")
 > 
-117c117
+119c119
 <    ((subst M x M_x) (subst N x M_x))]
 ---
 >    ((subst M x M_x) (subst N x M))]
-255a256
+257a258
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
deleted file mode 100644
index bdebba0522..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
+++ /dev/null
@@ -1,21 +0,0 @@
-3,4d2
-< (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "substitutes inside of λ that binds the sub variable")
-> 
-108,109d107
-<   [(subst (λ (x τ) M) x M_x)
-<    (λ (x τ) M)]
-114,115d111
-<   [(subst (c M) x M_x)
-<    (c (subst M x M_x))]
-117a114,115
->   [(subst (c M) x M_x)
->    (c (subst M x M_x))]
-255a254
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff
deleted file mode 100644
index 1881a73ce3..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/5.diff
+++ /dev/null
@@ -1,12 +0,0 @@
-3,4d2
-< (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "picks up the bound variable when recurring inside λ")
-> 
-254a255
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff
deleted file mode 100644
index cb47d8ae0d..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/6.diff
+++ /dev/null
@@ -1,12 +0,0 @@
-3,4d2
-< (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "swaps the bound var when recurring inside λ")
-> 
-254a255
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
index d2327a5e2c..ad0dc5a74c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
@@ -8,9 +8,9 @@
 12a11,12
 > (define the-error "swaps to/from expressions when recurring inside a constant")
 > 
-115c115
+117c117
 <    (c (subst M x M_x))]
 ---
 >    (c (subst M_x x M))]
-255a256
+257a258
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
deleted file mode 100644
index 6b8b695819..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
+++ /dev/null
@@ -1,16 +0,0 @@
-3,4d2
-< (define the-error "no error")
-< 
-7d4
-<          racket/match
-8a6
->          racket/match
-12a11,12
-> (define the-error "swaps the order of the λ clauses")
-> 
-108,109d107
-<   [(subst (λ (x τ) M) x M_x)
-<    (λ (x τ) M)]
-113a112,113
->   [(subst (λ (x τ) M) x M_x)
->    (λ (x τ) M)]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
index f74321b8ac..f9e10f5d93 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
@@ -11,8 +11,8 @@
 113a114,115
 >   [(subst (M N) x M_x)
 >    ((subst M_x x M) (subst N x M_x))]
-116,117d117
+118,119d119
 <   [(subst (M N) x M_x)
 <    ((subst M x M_x) (subst N x M_x))]
-255a256
+257a258
 > 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
index 0fc29e5a04..f49511fa3b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
-     (cons number)
-     ((cons number) v))
+     (cons v)
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,8 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
-
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define-metafunction stlc
   subst : M x M -> M
@@ -239,18 +241,21 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
+
      M]
     [#f #f]))
 
@@ -319,4 +324,3 @@
     ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
     
     )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
deleted file mode 100644
index d3301d3dff..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
+++ /dev/null
@@ -1,321 +0,0 @@
-#lang racket/base
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/list
-         racket/match
-         racket/contract
-         math/base)
-
-(provide (all-defined-out))
-(define the-error "only substitutes inside of hd constants")
-
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     number
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     number
-     (cons number)
-     ((cons number) v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------
-   (typeof Γ number int)]
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")))
-
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (hd M) x M_x)
-   (hd (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx should this also be t-type IMPLIES?
-        (and
-         (= (length red-res) 1)
-         (let ([red-t (car red-res)])
-           (or 
-            (equal? red-t "error")
-            (let ([red-type (type-check red-t)])
-              (equal? t-type red-type))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
index bbcc3211fe..4d95f8ef0c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
-     (cons number)
-     ((cons number) v))
+     (cons v)
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,8 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
-
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define-metafunction stlc
   subst : M x M -> M
@@ -239,18 +241,21 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
+
      M]
     [#f #f]))
 
@@ -319,4 +324,3 @@
     ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
     
     )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
deleted file mode 100644
index a6b02af375..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
+++ /dev/null
@@ -1,320 +0,0 @@
-#lang racket/base
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/list
-         racket/match
-         racket/contract
-         math/base)
-
-(provide (all-defined-out))
-(define the-error "substitutes inside of λ that binds the sub variable")
-
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     number
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     number
-     (cons number)
-     ((cons number) v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------
-   (typeof Γ number int)]
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")))
-
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx should this also be t-type IMPLIES?
-        (and
-         (= (length red-res) 1)
-         (let ([red-t (car red-res)])
-           (or 
-            (equal? red-t "error")
-            (let ([red-type (type-check red-t)])
-              (equal? t-type red-type))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
deleted file mode 100644
index 5ae59042a2..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
+++ /dev/null
@@ -1,322 +0,0 @@
-#lang racket/base
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/list
-         racket/match
-         racket/contract
-         math/base)
-
-(provide (all-defined-out))
-(define the-error "picks up the bound variable when recurring inside λ")
-
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     number
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     number
-     (cons number)
-     ((cons number) v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------
-   (typeof Γ number int)]
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")))
-
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
-    [`(typeof • ,M ,τ)
-     M]
-
-    [#f #f]))
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx should this also be t-type IMPLIES?
-        (and
-         (= (length red-res) 1)
-         (let ([red-t (car red-res)])
-           (or 
-            (equal? red-t "error")
-            (let ([red-type (type-check red-t)])
-              (equal? t-type red-type))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
deleted file mode 100644
index 08be36d3f4..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
+++ /dev/null
@@ -1,322 +0,0 @@
-#lang racket/base
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/list
-         racket/match
-         racket/contract
-         math/base)
-
-(provide (all-defined-out))
-(define the-error "swaps the bound var when recurring inside λ")
-
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     number
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     number
-     (cons number)
-     ((cons number) v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------
-   (typeof Γ number int)]
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")))
-
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
-    [`(typeof • ,M ,τ)
-     M]
-
-    [#f #f]))
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx should this also be t-type IMPLIES?
-        (and
-         (= (length red-res) 1)
-         (let ([red-t (car red-res)])
-           (or 
-            (equal? red-t "error")
-            (let ([red-type (type-check red-t)])
-              (equal? t-type red-type))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
index b2eeb91d89..272585f00c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
-     (cons number)
-     ((cons number) v))
+     (cons v)
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,8 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
-
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define-metafunction stlc
   subst : M x M -> M
@@ -239,18 +241,21 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
+
      M]
     [#f #f]))
 
@@ -319,4 +324,3 @@
     ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
     
     )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
deleted file mode 100644
index b4522ee5ef..0000000000
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
+++ /dev/null
@@ -1,321 +0,0 @@
-#lang racket/base
-
-(require redex/reduction-semantics
-         (only-in redex/private/generate-term pick-an-index)
-         racket/list
-         racket/match
-         racket/contract
-         math/base)
-
-(provide (all-defined-out))
-(define the-error "swaps the order of the λ clauses")
-
-
-(define-language stlc
-  (M N ::= 
-     (λ (x σ) M)
-     (M N)
-     number
-     x
-     c)
-  (Γ (x σ Γ)
-     •)
-  (σ τ ::=
-     int
-     (list int)
-     (σ → τ))
-  (c d ::= cons nil hd tl)
-  ((x y) variable-not-otherwise-mentioned)
-  
-  (v (λ (x τ) M)
-     c
-     number
-     (cons number)
-     ((cons number) v))
-  (E hole
-     (E M)
-     (v E)))
-
-(define-judgment-form stlc
-  #:mode (typeof I I O)
-  #:contract (typeof Γ M σ)
-  
-  [---------------------
-   (typeof Γ number int)]
-  
-  [---------------------------
-   (typeof Γ c (const-type c))]
-  
-  [(where τ (lookup Γ x))
-   ----------------------
-   (typeof Γ x τ)]
-  
-  [(typeof (x σ Γ) M σ_2)
-   --------------------------------
-   (typeof Γ (λ (x σ) M) (σ → σ_2))]
-  
-  [(typeof Γ M (σ → σ_2))
-   (typeof Γ M_2 σ)
-   ----------------------
-   (typeof Γ (M M_2) σ_2)])
-
-(define-metafunction stlc
-  const-type : c -> σ
-  [(const-type nil)
-   (list int)]
-  [(const-type cons)
-   (int → ((list int) → (list int)))]
-  [(const-type hd)
-   ((list int) → int)]
-  [(const-type tl)
-   ((list int) → (list int))])
-
-(define-metafunction stlc
-  lookup : Γ x -> σ or #f
-  [(lookup (x σ Γ) x)
-   σ]
-  [(lookup (x σ Γ) x_2)
-   (lookup Γ x_2)]
-  [(lookup • x)
-   #f])
-
-(define red
-  (reduction-relation
-   stlc
-   (--> (in-hole E ((λ (x τ) M) v))
-        (in-hole E (subst M x v))
-        "βv")
-   (--> (in-hole E (hd ((cons v_1) v_2)))
-        (in-hole E v_1)
-        "hd")
-   (--> (in-hole E (tl ((cons v_1) v_2)))
-        (in-hole E v_2)
-        "tl")
-   (--> (in-hole E (hd nil))
-        "error"
-        "hd-err")
-   (--> (in-hole E (tl nil))
-        "error"
-        "tl-err")))
-
-
-(define-metafunction stlc
-  subst : M x M -> M
-  [(subst x x M)
-   M]
-  [(subst y x M)
-   y]
-  [(subst (λ (x_1 τ) M) x_2 v)
-   (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
-  [(subst (λ (x τ) M) x M_x)
-   (λ (x τ) M)]
-  [(subst (c M) x M_x)
-   (c (subst M x M_x))]
-  [(subst (M N) x M_x)
-   ((subst M x M_x) (subst N x M_x))]
-  [(subst M x M_x)
-   M])
-
-(define-metafunction stlc
-  [(replace (any_1 ...) x_1 x_new)
-   ((replace any_1 x_1 x_new) ...)]
-  [(replace x_1 x_1 x_new)
-   x_new]
-  [(replace any_1 x_1 x_new)
-   any_1])
-
-(define M? (redex-match stlc M))
-(define/contract (Eval M)
-  (-> M? (or/c M? "error"))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (unless (pair? M-t)
-    (error 'Eval "doesn't typecheck: ~s" M))
-  (define res (apply-reduction-relation* red M))
-  (unless (= 1 (length res))
-    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
-  (define ans (car res))
-  (if (equal? "error" ans)
-      "error"
-      (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
-        (unless (equal? M-t ans-t)
-          (error 'Eval "internal error: type soundness fails for ~s" M))
-        ans)))
-
-(define x? (redex-match stlc x))
-
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
-(define/contract (type-check M)
-  (-> M? (or/c τ? #f))
-  (define M-t (judgment-holds (typeof • ,M τ) τ))
-  (cond
-    [(empty? M-t)
-     #f]
-    [(null? (cdr M-t))
-     (car M-t)]
-    [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
-
-(test-equal (type-check (term 5))
-            (term int))
-(test-equal (type-check (term (5 5)))
-            #f)
-
-(define (progress-holds? M)
-  (if (type-check M)
-      (or (v? M)
-          (not (null? (apply-reduction-relation red (term ,M)))))
-      #t))
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-(define-metafunction stlc
-  [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
-   #t]
-  [(uses-bound-var? (x_0 ...) (λ (x τ) M))
-   (uses-bound-var? (x x_0 ...) M)]
-  [(uses-bound-var? (x ...) (M N))
-   ,(or (term (uses-bound-var? (x ...) M))
-        (term (uses-bound-var? (x ...) N)))]
-  [(uses-bound-var? (x ...) (cons M))
-   (uses-bound-var? (x ...) M)]
-  [(uses-bound-var? (x ...) any)
-   #f])
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
-(define-metafunction stlc
-  [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
-   #t]
-  [(applies-bv? (x_0 ...) (λ (x τ) M))
-   (applies-bv? (x x_0 ...) M)]
-  [(applies-bv? (x ...) (M N))
-   ,(or (term (applies-bv? (x ...) M))
-        (term (applies-bv? (x ...) N)))]
-  [(applies-bv? (x ...) (cons M))
-   (applies-bv? (x ...) M)]
-  [(applies-bv? (x ...) any)
-   #f])
-
-(define (reduction-step-count/func red v?)
-  (λ (term)
-    (let loop ([t term]
-               [n 0])
-      (define res (apply-reduction-relation red t))
-      (cond 
-        [(and (empty? res)
-              (v? t))
-         n]
-        [(and (empty? res)
-              (equal? t "error"))
-         n]
-        [(= (length res) 1)
-         (loop (car res) (add1 n))]
-        [else
-         (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
-
-(define reduction-step-count
-  (reduction-step-count/func red v?))
-
-(define (generate-M-term)
-  (generate-term stlc M 5))
-
-(define (generate-M-term-from-red)
-  (generate-term #:source red 5))
-
-(define (generate-typed-term)
-  (match (generate-term stlc 
-                        #:satisfying
-                        (typeof • M τ)
-                        5)
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-
-(define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
-    [`(typeof • ,M ,τ)
-     M]
-    [#f #f]))
-(define (typed-generator)
-  (let ([g (redex-generator stlc 
-                            (typeof • M τ)
-                            5)])
-    (λ () 
-      (match (g)
-        [`(typeof • ,M ,τ)
-         M]
-        [#f #f]))))
-
-(define (check term)
-  (or (not term)
-      (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx should this also be t-type IMPLIES?
-        (and
-         (= (length red-res) 1)
-         (let ([red-t (car red-res)])
-           (or 
-            (equal? red-t "error")
-            (let ([red-type (type-check red-t)])
-              (equal? t-type red-type))))))))
-
-(define (generate-enum-term)
-  (generate-term stlc M #:i-th (pick-an-index 0.0001)))
-
-(define (ordered-enum-generator)
-  (let ([index 0])
-    (λ ()
-      (begin0
-        (generate-term stlc M #:i-th index)
-        (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 1
-    ((λ (x int) x) 1)
-
-    ;; 9
-    ((λ (x (list int)) (tl x)) ((cons 1) nil))
-
-    ;; 2 -- xxx I don't think this is really an error because the (M
-    ;; N) case does everything that (c M) does since M can equal
-    ;; c. Otherwise the previous test case would work, because (tl x)
-    ;; would not be subst'd and it has no type
-
-    ;; 3
-    ((λ (x int) ((λ (y int) y) x)) 1)
-
-    ;; 4 -- xxx I don't think this is really an error because the
-    ;; normal λ rule always does renaming so this test below works
-    ;; fine and ends up with x1 in both places.
-
-    #;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
-
-    ;; 5 & 6 --- xxx These diffs are bogus because they don't actually
-    ;; make a change to any of the program.
-
-    ;; 7
-    ((λ (x int) (hd ((cons x) nil))) 1)
-
-    ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
-    
-    )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
index 4b34887a69..2584a83df9 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
-     (cons number)
-     ((cons number) v))
+     (cons v)
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,8 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
-
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define-metafunction stlc
   subst : M x M -> M
@@ -109,10 +111,10 @@
    (λ (x τ) M)]
   [(subst (λ (x_1 τ) M) x_2 v)
    (λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
-   (where x_new ,(variable-not-in (term (x_1 e x_2))
-                                  (term x_1)))]
   [(subst (M N) x M_x)
    ((subst M_x x M) (subst N x M_x))]
+   (where x_new ,(variable-not-in (term (x_1 e x_2))
+                                  (term x_1)))]
   [(subst (c M) x M_x)
    (c (subst M x M_x))]
   [(subst M x M_x)
@@ -239,18 +241,21 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
+
      M]
     [#f #f]))
 
@@ -319,4 +324,3 @@
     ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
     
     )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
index e8744360b7..b7a80aa555 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
-     (cons number)
-     ((cons number) v))
+     (cons v)
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,8 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
-
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define-metafunction stlc
   subst : M x M -> M
@@ -239,20 +241,23 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
+
 (define (typed-generator)
   (let ([g (redex-generator stlc 
                             (typeof • M τ)
@@ -318,4 +323,3 @@
     ;; 8 -- xxx This isn't an error for the same reason 4 isn't.
     
     )))
-
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/tests.rkt
new file mode 100644
index 0000000000..cfc58af124
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/tests.rkt
@@ -0,0 +1,7 @@
+#lang racket/base
+(require "stlc-sub-base.rkt" "../stlc/tests-lib.rkt")
+(stlc-tests uses-bound-var?
+            typeof
+            red
+            reduction-step-count
+            Eval)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
similarity index 59%
rename from pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff
rename to pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
index 23bcc13828..9e087369f3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/10.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
@@ -1,10 +1,12 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "app rule the range of the function is matched to the argument")
-58c58
+31a32
+>      ((cons v) v)
+53c54
 <    (typeof Γ M_2 σ)
 ---
 >    (typeof Γ M_2 σ_2)
-232d231
+236d236
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
index d024180321..13fe9f0baf 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/2.diff
@@ -1,9 +1,6 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the ((cons number) v) value has been omitted")
-33,34c33
-<      (cons v)
-<      ((cons v) v))
----
->      (cons v))
+31a32
+>      ((cons v) v)
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff
index 1932a76597..c4b6c2c525 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/3.diff
@@ -1,8 +1,10 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the order of the types in the function position of application has been swapped")
-57c57
+31a32
+>      ((cons v) v)
+52c53
 <   [(typeof Γ M (σ → σ_2))
 ---
 >   [(typeof Γ M (σ_2 → σ))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
index 1cebcca1f5..c96c800c34 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/4.diff
@@ -1,8 +1,10 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the type of cons is incorrect")
-67c67
+31a32
+>      ((cons v) v)
+62c63
 <    (int → ((list int) → (list int)))]
 ---
 >    (int → ((list int) → int))]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff
index dd35b1299c..2b2121c7a0 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/5.diff
@@ -1,10 +1,12 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the tail reduction returns the wrong value")
-92c92
+31a32
+>      ((cons v) v)
+91c92
 <         (in-hole E v_2)
 ---
 >         (in-hole E v_1)
-232d231
+236d236
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff
index c978fe3fba..0915cc3a21 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/6.diff
@@ -1,10 +1,12 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "hd reduction acts on partially applied cons")
-88c88
+31a32
+>      ((cons v) v)
+87c88
 <    (--> (in-hole E (hd ((cons v_1) v_2)))
 ---
 >    (--> (in-hole E (hd (cons v_1)))
-232d231
+236d236
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
index 5df0c31c62..cf4eadc771 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/7.diff
@@ -1,11 +1,13 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "evaluation isn't allowed on the rhs of applications")
-36,37c36
+31a32
+>      ((cons v) v)
+34,35c35
 <      (E M)
 <      (v E)))
 ---
 >      (E M)))
-232d230
+236d235
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff
index d18e4f37b9..2b7cbde09c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/8.diff
@@ -1,10 +1,12 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "lookup always returns int")
-76c76
+31a32
+>      ((cons v) v)
+75c76
 <    σ]
 ---
 >    int]
-232d231
+236d236
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff
index 99aaad3984..eb2cd9bd1c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/9.diff
@@ -1,10 +1,12 @@
 3c3
-< (define the-error "no error")
+< (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "variables aren't required to match in lookup")
-75c75
+31a32
+>      ((cons v) v)
+74c75
 <   [(lookup (x σ Γ) x)
 ---
 >   [(lookup (x σ Γ) x_2)
-232d231
+236d236
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
similarity index 87%
rename from pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt
rename to pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
index 6194c5ae97..816482aa01 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt
index b48aa96393..3159314164 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-2.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,13 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
-     (cons v))
+     (cons v)
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -39,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -67,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -95,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -214,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt
index 5615fa769f..0a501d2385 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-3.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
index 06e5de57dd..acd6d6c83e 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-4.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt
index 10bfba6605..39a6c44320 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-5.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt
index 7e7d7d1be3..5083763804 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-6.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
index 9360bee92f..13d515f4a4 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-7.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)))
 
@@ -39,9 +38,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -67,7 +63,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -95,7 +95,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -214,17 +217,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt
index 8ee7b2cf14..a6378c4087 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-8.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt
index 6aaf98f71c..01e9cf0ea2 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-9.rkt
@@ -4,8 +4,8 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,14 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     ((cons v) v)
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +39,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +64,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +96,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +218,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt
index b62eeaeb1c..b942d58c44 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-base.rkt
@@ -1,11 +1,11 @@
 #lang racket/base
 
-(define the-error "no error")
+(define the-error "the ((cons v) v) value has been omitted")
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
          racket/match
+         racket/list
          racket/contract
          "tut-subst.rkt")
 
@@ -15,7 +15,6 @@
   (M N ::= 
      (λ (x σ) M)
      (M N)
-     number
      x
      c)
   (Γ (x σ Γ)
@@ -24,14 +23,13 @@
      int
      (list int)
      (σ → τ))
-  (c d ::= cons nil hd tl)
+  (c d ::= cons nil hd tl + integer)
   ((x y) variable-not-otherwise-mentioned)
   
   (v (λ (x τ) M)
      c
-     number
      (cons v)
-     ((cons v) v))
+     (+ v))
   (E hole
      (E M)
      (v E)))
@@ -40,9 +38,6 @@
   #:mode (typeof I I O)
   #:contract (typeof Γ M σ)
   
-  [---------------------
-   (typeof Γ number int)]
-  
   [---------------------------
    (typeof Γ c (const-type c))]
   
@@ -68,7 +63,11 @@
   [(const-type hd)
    ((list int) → int)]
   [(const-type tl)
-   ((list int) → (list int))])
+   ((list int) → (list int))]
+  [(const-type +)
+   (int → (int → int))]
+  [(const-type integer)
+   int])
 
 (define-metafunction stlc
   lookup : Γ x -> σ or #f
@@ -96,7 +95,10 @@
         "hd-err")
    (--> (in-hole E (tl nil))
         "error"
-        "tl-err")))
+        "tl-err")
+   (--> (in-hole E ((+ integer_1) integer_2))
+        (in-hole E ,(+ (term integer_1) (term integer_2)))
+        "+")))
 
 (define M? (redex-match stlc M))
 (define/contract (Eval M)
@@ -215,17 +217,19 @@
     [#f #f]))
 
 (define (generate-typed-term-from-red)
-  (match (case (random 5)
-           [(0)
-            (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
-           [(1)
-            (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(2)
-            (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
-           [(3)
-            (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
-           [(4)
-            (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
+  (define candidate
+    (case (random 5)
+      [(0)
+       (generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
+      [(1)
+       (generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(2)
+       (generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
+      [(3)
+       (generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
+      [(4)
+       (generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
+  (match candidate
     [`(typeof • ,M ,τ)
      M]
     [#f #f]))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt
new file mode 100644
index 0000000000..7cfea71737
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt
@@ -0,0 +1,102 @@
+#lang racket/base
+(require redex/reduction-semantics)
+(provide stlc-tests)
+
+(define-syntax-rule
+  (stlc-tests uses-bound-var?
+              typeof
+              red
+              reduction-step-count
+              Eval)
+  (begin
+    
+    (test-equal (term (uses-bound-var? () 5))
+                #f)
+    (test-equal (term (uses-bound-var? () nil))
+                #f)
+    (test-equal (term (uses-bound-var? () (λ (x int) x)))
+                #t)
+    (test-equal (term (uses-bound-var? () (λ (x int) y)))
+                #f)
+    (test-equal (term (uses-bound-var? () ((λ (x int) x) 5)))
+                #t)
+    (test-equal (term (uses-bound-var? () ((λ (x int) xy) 5)))
+                #f)
+    
+    (test-equal (judgment-holds (typeof • 5 τ) τ)
+                (list (term int)))
+    (test-equal (judgment-holds (typeof • nil τ) τ)
+                (list (term (list int))))
+    (test-equal (judgment-holds (typeof • (cons 1) τ) τ)
+                (list (term ((list int) → (list int)))))
+    (test-equal (judgment-holds (typeof • ((cons 1) nil) τ) τ)
+                (list (term (list int))))
+    (test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
+                (list (term (int → int))))
+    (test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
+                (list (term ((int → int) → (int → (int → int))))))
+    (test-equal (judgment-holds (typeof • ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
+                (list (term int)))
+    
+    (test-->> red (term ((λ (x int) x) 7)) (term 7))
+    (test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
+    (test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
+    (test-->> red 
+              (term ((λ (x int) ((cons x) nil)) 11))
+              (term ((cons 11) nil)))
+    (test-->> red 
+              (term ((λ (x int) ((cons x) nil)) 11))
+              (term ((cons 11) nil)))
+    (test-->> red 
+              (term ((cons ((λ (x int) x) 11)) nil))
+              (term ((cons 11) nil)))
+    (test-->> red
+              (term (cons ((λ (x int) x) 1)))
+              (term (cons 1)))
+    (test-->> red
+              (term ((cons ((λ (x int) x) 1)) nil))
+              (term ((cons 1) nil)))
+    (test-->> red
+              (term (hd ((λ (x int) ((cons x) nil)) 11)))
+              (term 11))
+    (test-->> red
+              (term (tl ((λ (x int) ((cons x) nil)) 11)))
+              (term nil))
+    (test-->> red
+              (term (tl nil))
+              "error")
+    (test-->> red
+              (term (hd nil))
+              "error")
+    (test-->> red
+              (term ((+ 1) (hd nil)))
+              "error")
+    (test-->> red
+              (term ((+ ((+ 1) 2)) ((+ 3) 4)))
+              (term 10))
+    (test-->> red
+              (term ((λ (f (int → (list int))) (f 3)) (cons 1)))
+              (term ((cons 1) 3)))
+    (test-->> red
+              (term ((λ (f (int → int)) (f 3)) (+ 1)))
+              (term 4))
+              
+    (test-equal (Eval (term ((λ (x int) x) 3)))
+                (term 3))
+    
+    (test-equal (reduction-step-count (term (λ (x int) x)))
+                0)
+    (test-equal (reduction-step-count (term ((λ (x int) x) 1)))
+                1)
+    (test-equal (reduction-step-count (term ((λ (x int) x) 1)))
+                1)
+    (test-equal (reduction-step-count (term ((cons 1) nil)))
+                0)
+    (test-equal (reduction-step-count (term (hd ((cons 1) nil))))
+                1)
+    (test-equal (reduction-step-count (term (hd nil)))
+                1)
+    (test-equal (reduction-step-count (term ((λ (x int) x) (hd ((cons 1) nil)))))
+                2)
+    
+    (test-results)))
\ No newline at end of file
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests.rkt
index 4c882c9392..ce4ef9180a 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests.rkt
@@ -1,81 +1,7 @@
 #lang racket/base
-
-(require redex/reduction-semantics
-         "stlc-base.rkt")
-
-(test-equal (term (uses-bound-var? () 5))
-            #f)
-(test-equal (term (uses-bound-var? () nil))
-            #f)
-(test-equal (term (uses-bound-var? () (λ (x int) x)))
-            #t)
-(test-equal (term (uses-bound-var? () (λ (x int) y)))
-            #f)
-(test-equal (term (uses-bound-var? () ((λ (x int) x) 5)))
-            #t)
-(test-equal (term (uses-bound-var? () ((λ (x int) xy) 5)))
-            #f)
-
-(test-equal (judgment-holds (typeof • 5 τ) τ)
-            (list (term int)))
-(test-equal (judgment-holds (typeof • nil τ) τ)
-            (list (term (list int))))
-(test-equal (judgment-holds (typeof • (cons 1) τ) τ)
-            (list (term ((list int) → (list int)))))
-(test-equal (judgment-holds (typeof • ((cons 1) nil) τ) τ)
-            (list (term (list int))))
-(test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
-            (list (term (int → int))))
-(test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
-            (list (term ((int → int) → (int → (int → int))))))
-
-(test-->> red (term ((λ (x int) x) 7)) (term 7))
-(test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
-(test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
-(test-->> red 
-          (term ((λ (x int) ((cons x) nil)) 11))
-          (term ((cons 11) nil)))
-(test-->> red 
-          (term ((λ (x int) ((cons x) nil)) 11))
-          (term ((cons 11) nil)))
-(test-->> red 
-          (term ((cons ((λ (x int) x) 11)) nil))
-          (term ((cons 11) nil)))
-(test-->> red
-          (term (cons ((λ (x int) x) 1)))
-          (term (cons 1)))
-(test-->> red
-          (term ((cons ((λ (x int) x) 1)) nil))
-          (term ((cons 1) nil)))
-(test-->> red
-          (term (hd ((λ (x int) ((cons x) nil)) 11)))
-          (term 11))
-(test-->> red
-          (term (tl ((λ (x int) ((cons x) nil)) 11)))
-          (term nil))
-(test-->> red
-          (term (tl nil))
-          "error")
-(test-->> red
-          (term (hd nil))
-          "error")
-
-(test-equal (Eval (term ((λ (x int) x) 3)))
-            (term 3))
-
-(test-equal (reduction-step-count (term (λ (x int) x)))
-            0)
-(test-equal (reduction-step-count (term ((λ (x int) x) 1)))
-            1)
-(test-equal (reduction-step-count (term ((λ (x int) x) 1)))
-            1)
-(test-equal (reduction-step-count (term ((cons 1) nil)))
-            0)
-(test-equal (reduction-step-count (term (hd ((cons 1) nil))))
-            1)
-(test-equal (reduction-step-count (term (hd nil)))
-            1)
-(test-equal (reduction-step-count (term ((λ (x int) x) (hd ((cons 1) nil)))))
-            2)
-
-(test-results)
\ No newline at end of file
+(require "stlc-base.rkt" "tests-lib.rkt")
+(stlc-tests uses-bound-var?
+            typeof
+            red
+            reduction-step-count
+            Eval)