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 57ed671a31..2f2113a4e4 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -248,14 +249,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -266,25 +268,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 a0524740c7..bb2d576d51 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -249,14 +250,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -267,25 +269,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 706da6752e..a0606ab9c6 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -249,14 +250,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -267,25 +269,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 c75c729903..22e33222d3 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -249,14 +250,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -267,25 +269,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 652c2d72fe..0364a3f661 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -248,14 +249,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -266,25 +268,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 b610203301..2eb0ce335f 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -248,14 +249,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -266,25 +268,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 f1b0139f16..1f6f3e176f 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -247,14 +248,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -265,25 +267,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 3505c25c9b..3b2fc72df2 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -248,14 +249,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -266,25 +268,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 f8d1902ba9..c8b605ec15 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
@@ -7,6 +7,7 @@
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -248,14 +249,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -266,25 +268,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))
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 4e281bd778..ccc37c6faf 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,12 +1,13 @@
 #lang racket/base
 
-(define the-error "the ((cons v) v) value has been omitted")
+(define the-error "no error")
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
          racket/match
          racket/list
          racket/contract
+         racket/bool
          "tut-subst.rkt")
 
 (provide (all-defined-out))
@@ -248,14 +249,15 @@
 (define (check term)
   (or (not term)
       (v? term)
-      (let ([red-res (apply-reduction-relation red term)]
-            [t-type (type-check term)])
-        ;; xxx shouldn't this be t-type IMPLIES this?
-        (and
-         (= (length red-res) 1)
-         (or 
-          (equal? (car red-res) "error")
-          (equal? t-type (type-check (car red-res))))))))
+      (let ([t-type (type-check term)])
+        (implies
+         t-type
+         (let ([red-res (apply-reduction-relation red term)])
+           (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.035)))
@@ -266,25 +268,3 @@
       (begin0
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
-
-(define fixed
-  (term
-   (;; 2
-    ((cons 1) nil)
-    ;; 3
-    ((λ (x (list int)) 1) 
-     7)
-    ;; 4 (if we hadn't changed number->v in cons)
-    (cons ((cons 0) nil))
-    ;; 5
-    (tl ((cons 1) nil))
-    ;; 6
-    (hd ((cons 1) nil))
-    ;; 7
-    ((λ (x int) x) (hd ((cons 1) nil)))
-    ;; 8
-    ((λ (x (list int)) (cons x)) nil)
-    ;; 9
-    ((λ (x int) (λ (y (list int)) x)) 1)
-    ;; 10
-    (hd 0))))