diff --git a/collects/redex/examples/church.ss b/collects/redex/examples/church.ss
index 06aa2fa0ad..b3152a11b5 100644
--- a/collects/redex/examples/church.ss
+++ b/collects/redex/examples/church.ss
@@ -5,17 +5,18 @@
 
 (define-language lang
   (e (lambda (x) e)
-     (e e)
+     (let (x e) e)
+     (app e e)
      (+ e e)
      number
      x)
-  (ctxt (ctxt e)
-          (v ctxt)
-          (+ ctxt e)
-          (+ v ctxt)
+  (e-ctxt (lambda (x) e-ctxt)
+          a-ctxt)
+  (a-ctxt (let (x a-ctxt) e)
+          (app a-ctxt e)
+          (app x a-ctxt)
           hole)
   (v (lambda (x) e)
-     number
      x)
   (x variable))
 
@@ -46,4 +47,11 @@
       (subst (x_1 e_1 e_3)))]
   [(subst (x_1 e_1 number_1)) number_1])
 
-(apply-reduction-relation reductions `(app (lambda (x) x) (lambda (x) x)))
+(traces reductions
+        '(let (plus (lambda (m) 
+                      (lambda (n) 
+                        (lambda (s)
+                          (lambda (z)
+                            (app (app m s) (app (app n s) z)))))))
+           (let (two (lambda (s) (lambda (z) (app s (app s z)))))
+             (app (app plus two) two))))