diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
index 9e087369f3..9e3142e70e 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/1.diff
@@ -2,11 +2,11 @@
 < (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")
-31a32
+32a33
 >      ((cons v) v)
-53c54
+54c55
 <    (typeof Γ M_2 σ)
 ---
 >    (typeof Γ M_2 σ_2)
-236d236
+237d237
 < 
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 13fe9f0baf..67e4aca243 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
@@ -2,5 +2,5 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the ((cons number) v) value has been omitted")
-31a32
+32a33
 >      ((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 c4b6c2c525..871e87633f 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
@@ -2,9 +2,9 @@
 < (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")
-31a32
+32a33
 >      ((cons v) v)
-52c53
+53c54
 <   [(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 c96c800c34..87aa4cf3f6 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
@@ -2,9 +2,9 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the type of cons is incorrect")
-31a32
+32a33
 >      ((cons v) v)
-62c63
+63c64
 <    (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 2b2121c7a0..d6938054d0 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
@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "the tail reduction returns the wrong value")
-31a32
+32a33
 >      ((cons v) v)
-91c92
+92c93
 <         (in-hole E v_2)
 ---
 >         (in-hole E v_1)
-236d236
+237d237
 < 
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 0915cc3a21..23c53af16d 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
@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "hd reduction acts on partially applied cons")
-31a32
+32a33
 >      ((cons v) v)
-87c88
+88c89
 <    (--> (in-hole E (hd ((cons v_1) v_2)))
 ---
 >    (--> (in-hole E (hd (cons v_1)))
-236d236
+237d237
 < 
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 cf4eadc771..005d6ca28f 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
@@ -2,12 +2,12 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "evaluation isn't allowed on the rhs of applications")
-31a32
+32a33
 >      ((cons v) v)
-34,35c35
+35,36c36
 <      (E M)
 <      (v E)))
 ---
 >      (E M)))
-236d235
+237d236
 < 
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 2b7cbde09c..4174e2d55c 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
@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "lookup always returns int")
-31a32
+32a33
 >      ((cons v) v)
-75c76
+76c77
 <    σ]
 ---
 >    int]
-236d236
+237d237
 < 
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 eb2cd9bd1c..bd53e96341 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
@@ -2,11 +2,11 @@
 < (define the-error "the ((cons v) v) value has been omitted")
 ---
 > (define the-error "variables aren't required to match in lookup")
-31a32
+32a33
 >      ((cons v) v)
-74c75
+75c76
 <   [(lookup (x σ Γ) x)
 ---
 >   [(lookup (x σ Γ) x_2)
-236d236
+237d237
 < 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
index 816482aa01..1a5fe2efa2 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 3159314164..c37526309f 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 0a501d2385..81b7a859cb 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 acd6d6c83e..aa51f4443d 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 39a6c44320..b8fd50fadc 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 5083763804..f9be03c38b 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 13d515f4a4..9c7265257f 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)))
@@ -123,8 +124,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 a6378c4087..5feebae2ee 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 01e9cf0ea2..3a7e8dbcca 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
@@ -30,6 +30,7 @@
      c
      (cons v)
      ((cons v) v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -124,8 +125,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))
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 b942d58c44..9a3ce8741c 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
@@ -29,6 +29,7 @@
   (v (λ (x τ) M)
      c
      (cons v)
+     ((cons v) v)
      (+ v))
   (E hole
      (E M)
@@ -123,8 +124,8 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match stlc v))
-(define τ? (redex-match stlc τ))
+(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 τ) τ))