diff --git a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
index 45e0f2b5..819244cc 100644
--- a/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
+++ b/redex-doc/redex/scribblings/long-tut/mon-aft.scrbl
@@ -207,7 +207,10 @@ Here are two more metafunctions that use patterns in interesting ways:
    (where #false (in x (x_1 ...)))]
   [(subtract1 (x ...) x_1) (x ...)])
 
-
+(define-metafunction Lambda
+  in : x (x ...) -> boolean
+  [(in x (x_1 ... x x_2 ...)) #true]
+  [(in x (x_1 ...)) #false])
 
 ))
 @;%
@@ -319,15 +322,9 @@ Now α equivalence is straightforward:
 (racketblock
 ;; (=α e_1 e_2) determines whether e_1 and e_2 are α equivalent
 
-(define-extended-language Lambda/n Lambda
-  (e ::= .... n)
-  (n ::= natural))
-
-(define in-Lambda/n? (redex-match? Lambda/n e))
-
 (module+ test
   (test-equal (term (=α (lambda (x) x) (lambda (y) y))) #true)
-  (test-equal (term (=α (lambda (x) (x 1)) (lambda (y) (y 1)))) #true)
+  (test-equal (term (=α (lambda (x) (x x)) (lambda (y) (y y)))) #true)
   (test-equal (term (=α (lambda (x) x) (lambda (y) z))) #false))
 
 (define-metafunction SD