diff --git a/collects/redex/examples/list-machine/list-machine-typing.rkt b/collects/redex/examples/list-machine/list-machine-typing.rkt
index a2f21deba7..efadf995f4 100644
--- a/collects/redex/examples/list-machine/list-machine-typing.rkt
+++ b/collects/redex/examples/list-machine/list-machine-typing.rkt
@@ -92,7 +92,7 @@
   [(:lookup Γ v (listcons τ)) (:set Γ v_2 (list τ) Γ_2)
    -----
    (check-instr Π Γ (fetch-field v 1 v_2) Γ_2)]
-  [(:lookup Γ v_0 τ_0) (:lookup Γ v_0 τ_1)
+  [(:lookup Γ v_0 τ_0) (:lookup Γ v_1 τ_1)
    (⊔ (list τ_0) τ_1 (list τ)) (:set Γ v (listcons τ) Γ_2)
    -----
    (check-instr Π Γ (cons v_0 v_1 v) Γ_2)])
diff --git a/collects/redex/examples/list-machine/test.rkt b/collects/redex/examples/list-machine/test.rkt
index d8cbf458f9..5d06835d3d 100644
--- a/collects/redex/examples/list-machine/test.rkt
+++ b/collects/redex/examples/list-machine/test.rkt
@@ -132,6 +132,12 @@
                            (y : (list (list nil)) 
                               (z : (listcons (list nil))
                                  empty))))))
+(test-equal (judgment-holds (check-instr
+                             (l0 : (v0 : nil empty) empty)
+                             (v0 : nil empty)
+                             (cons v0 x f)
+                             Γ))
+            #f)
 
 (test-equal (judgment-holds (check-block empty empty halt)) #t)
 (test-equal (judgment-holds (check-block empty