diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/1.diff
index 8833a15243..bd0a70cc2c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/1.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "app rule the range of the function is matched to the argument")
-73c73
+74c74
 <   [(typeof Γ M (σ → σ_2))
 ---
 >   [(typeof Γ M (σ_2 → σ_2))
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff
index 7828d2587b..003937e930 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff
@@ -2,9 +2,9 @@
 < (define the-error "no error")
 ---
 > (define the-error "the (([cons @ τ] v) v) value has been omitted")
-47d46
+48d47
 <      (([cons @ τ] v) v)
-262,263c261
+261,262c260
 <       M]
 <     [#f #f]))
 ---
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff
index fcffd11709..29bf4a87b3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "the order of the types in the function position of application has been swapped")
-73c73
+74c74
 <   [(typeof Γ M (σ → σ_2))
 ---
 >   [(typeof Γ M (σ_2 → σ))
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff
index a718d7e909..e61b376c52 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "the type of cons is incorrect")
-120c120
+124c124
 <    (∀ a (a → ((list a) → (list a))))]
 ---
 >    (∀ a (a → ((list a) → a)))]
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff
index c82b84ceb8..5b5b392dd9 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "the tail reduction returns the wrong value")
-166c166
+172c172
 <         (in-hole E v_2)
 ---
 >         (in-hole E v_1)
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff
index 70fcc31c17..b168ba5461 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "hd reduction acts on partially applied cons")
-162c162
+168c168
 <    (--> (in-hole E ((hd @ τ) (((cons @ τ) v_1) v_2)))
 ---
 >    (--> (in-hole E ((hd @ τ) ((cons @ τ) v_1)))
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff
index 7d0a06b54a..1bcd0b447f 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff
@@ -2,12 +2,12 @@
 < (define the-error "no error")
 ---
 > (define the-error "evaluation isn't allowed on the rhs of applications")
-50,51c50
+51,52c51
 <      (E M)
 <      (v E)))
 ---
 >      (E M)))
-262c261
+261c260
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff
index 097e2a9774..4b349ec727 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "lookup always returns int")
-109c109
+113c113
 <    σ]
 ---
 >    int]
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff
index 842f9f2b1e..ec426a3532 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff
@@ -2,11 +2,11 @@
 < (define the-error "no error")
 ---
 > (define the-error "variables aren't required to match in lookup")
-108c108
+112c112
 <   [(lookup (x σ Γ) x)
 ---
 >   [(lookup (x σ Γ) x_2)
-262c262
+261c261
 <       M]
 ---
 >      M]
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
index 9561ec7160..dd820d319d 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
index 3517e3b13a..054236f168 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      ([[map @ τ_1] @ τ_2] v))
   (E hole
@@ -92,7 +93,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -122,7 +126,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -175,7 +181,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 poly-stlc M))
 (define/contract (Eval M)
@@ -213,16 +222,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
index 41f419471c..ebaf97c6fd 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
index 56632a6726..b8b2cdee06 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
index 4c8e92154c..23b08ad017 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
index ae26a41da5..584b43692c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
index c8516eeeb2..0867ad275c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -92,7 +93,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -122,7 +126,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -175,7 +181,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 poly-stlc M))
 (define/contract (Eval M)
@@ -213,16 +222,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
index ba70702d59..23a4a33274 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
index a62e7dd1e4..1b227f7e67 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
index 482ad6d37d..45b01d2a8b 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
@@ -16,7 +16,7 @@
      (λ (x σ) M)
      (M N)
      C
-     number
+     integer
      x)
   (C ::=
      [C @ σ]
@@ -38,11 +38,12 @@
      γ)
   (x y ::= variable-not-otherwise-mentioned)
   (α β ::= variable-not-otherwise-mentioned)
-  (c d ::= map nil cons hd tl)
+  (c d ::= map nil cons hd tl +)
   
   (v (λ (x τ) M)
      C
-     number
+     integer
+     (+ v)
      ([cons @ τ] v)
      (([cons @ τ] v) v)
      ([[map @ τ_1] @ τ_2] v))
@@ -93,7 +94,10 @@
   ; (where σ (t-subst2 γ α τ_1 β τ_2))
   ; ------------------------------
   ; (typeof-C [[c @ τ_1] @ τ_2] σ)]
-  )
+  
+  [(where γ (const-type c))
+   ------------------------------
+   (typeof-C c γ)])
 
 (define-extended-judgment-form poly-stlc typeof
   #:mode (typ-ind I I O)
@@ -123,7 +127,9 @@
   [(const-type tl)
    (∀ a ((list a) → (list a)))]
   [(const-type map)
-   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))])
+   (∀ α (∀ β ((α → β) → ((list α) → (list β)))))]
+  [(const-type +)
+   (int → (int → int))])
 
 (define-metafunction poly-stlc
   t-subst : γ α τ -> γ
@@ -176,7 +182,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 poly-stlc M))
 (define/contract (Eval M)
@@ -214,16 +223,6 @@
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-
-(define (interesting-term? M)
-  (and (type-check M)
-       (term (uses-bound-var? () ,M))))
-
-
-(define (really-interesting-term? M)
-  (and (interesting-term? M)
-       (term (applies-bv? () ,M))))
-
 (define (generate-M-term)
   (generate-term poly-stlc M 5))
 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt
index f3a780f955..0445328f5c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt
@@ -92,10 +92,6 @@
             (term 3))
 
 
-
-#|
-;; tests for arithmetic; not yet added to the model.
-
 (test-equal (judgment-holds (typeof • ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
             (list (term int)))
 (test-->> red
@@ -107,6 +103,5 @@
 (test-->> red
           (term ((λ (f (int → int)) (f 3)) (+ 1)))
           (term 4))
-|#
 
 (test-results)