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 003937e930..2581c28b16 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
@@ -9,3 +9,7 @@
 <     [#f #f]))
 ---
 >      M]))
+294a293,295
+> (define small-counter-example (term (([cons @ int] 1) [nil @ int])))
+> (test-equal (check small-counter-example) #f)
+> 
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 dd820d319d..92bc6d5690 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 054236f168..284164773e 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -209,13 +209,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -266,19 +266,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
@@ -290,6 +290,9 @@
         (generate-term poly-stlc M #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example (term (([cons @ int] 1) [nil @ int])))
+(test-equal (check small-counter-example) #f)
+
 (define fixed
   (term
    (;; 2
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 ebaf97c6fd..15375ef40e 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 b8b2cdee06..3f53ec04d7 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 23b08ad017..3dde3ed242 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 584b43692c..b0260c0958 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 0867ad275c..380606d1bb 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -209,13 +209,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -267,19 +267,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 23a4a33274..91af52bba9 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 1b227f7e67..2711262189 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))
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 45b01d2a8b..a4da3d70fa 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
@@ -2,7 +2,7 @@
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
-         racket/list
+         racket/bool
          racket/match
          racket/contract
          "tut-subst.rkt")
@@ -210,13 +210,13 @@
   [(subst M x N) 
    ,(subst/proc x? (term (x)) (term (N)) (term M))])
 
-(define v? (redex-match poly-stlc v))
-(define τ? (redex-match poly-stlc τ))
+(define v? (redex-match? poly-stlc v))
+(define τ? (redex-match? poly-stlc τ))
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof • ,M τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-t)
      #f]
     [(null? (cdr M-t))
      (car M-t)]
@@ -268,19 +268,19 @@
          M]
         [#f #f]))))
 
+;; check : (or/c #f M[from poly-stlc language]) -> boolean[#f = counterexample found!]
 (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))))))))
+      (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 poly-stlc M #:i-th (pick-an-index 0.065)))