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
index 63e41c63ef..72d3c27d71 100644
--- 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
@@ -8,6 +8,6 @@
 >   [(subst x y M_x)
 298a299,302
 > (define small-counter-example
->   (term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
+>   (term (λ (x int) ((λ (x int) x) x))))
 > (test-equal (check small-counter-example) #f)
 > 
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 3a4858f8bd..5fa3b595ec 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
@@ -45,6 +45,6 @@
 >                         (equal? t-type red-type))))))))))
 298a288,291
 > (define small-counter-example
->   (term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
+>   (term ((λ (a (list int)) (λ (x int) x)) nil)))
 > (test-equal (check small-counter-example) #f)
 > 
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
index de1c497057..af9ec23c93 100644
--- 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
@@ -297,7 +297,7 @@
   (generate-term stlc M #:i-th (pick-an-index 0.035)))
 
 (define small-counter-example
-  (term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
+  (term (λ (x int) ((λ (x int) x) x))))
 (test-equal (check small-counter-example) #f)
 
 (define (ordered-enum-generator)
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 e4cb2ec86f..8e2934c4d0 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
@@ -286,7 +286,7 @@
   (generate-term stlc M #:i-th (pick-an-index 0.035)))
 
 (define small-counter-example
-  (term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
+  (term ((λ (a (list int)) (λ (x int) x)) nil)))
 (test-equal (check small-counter-example) #f)
 
 (define (ordered-enum-generator)
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 ef95d05819..d766bc6a45 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
@@ -9,5 +9,5 @@
 270a271,274
 > 
 > (define small-counter-example
->   (term ((λ (x (list int)) 1) 7)))
+>   (term ((λ (x int) cons) cons)))
 > (test-equal (check small-counter-example) #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 58d11a8bf5..59c89408c9 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
@@ -270,5 +270,5 @@
         (set! index (add1 index))))))
 
 (define small-counter-example
-  (term ((λ (x (list int)) 1) 7)))
+  (term ((λ (x int) cons) cons)))
 (test-equal (check small-counter-example) #f)