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 1c497f5830..ddc26856f1 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
@@ -6,3 +6,8 @@
 <   [(lookup (x σ Γ) x)
 ---
 >   [(lookup (x σ Γ) x_2)
+294a295,298
+> (define small-counter-example
+>   (term ((λ (y (list int)) ([hd @ int] x))
+>          [nil @ int])))
+> (test-equal (check small-counter-example) #f)
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 2aac696991..5939fa1db9 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
@@ -292,3 +292,7 @@
         (generate-term poly-stlc M #:i-th index)
         (set! index (add1 index))))))
 
+(define small-counter-example
+  (term ((λ (y (list int)) ([hd @ int] x))
+         [nil @ int])))
+(test-equal (check small-counter-example) #f)