diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
index 59d6181..26a7bb1 100644
--- a/tapl/stlc+box.rkt
+++ b/tapl/stlc+box.rkt
@@ -1,9 +1,9 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app λ))
-         (except-in "stlc+cons.rkt" #%app λ))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+cons.rkt") stlc:#%app stlc:λ))
+(require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app))
+         (except-in "stlc+cons.rkt" #%app))
+(provide (rename-out [stlc:#%app #%app]))
+(provide (except-out (all-from-out "stlc+cons.rkt") stlc:#%app))
 (provide ref deref :=)
 
 ;; Simply-Typed Lambda Calculus, plus mutable references
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 684b4d0..7cf6243 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -1,10 +1,9 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+var.rkt" #%app λ let begin))
-         (except-in "stlc+var.rkt" #%app λ let begin))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let] [stlc:begin begin]
-                     [cons/tc cons] [define/tc define]))
-(provide (except-out (all-from-out "stlc+var.rkt") stlc:#%app stlc:λ stlc:let stlc:begin))
+(require (prefix-in stlc: (only-in "stlc+var.rkt" #%app))
+         (except-in "stlc+var.rkt" #%app))
+(provide (rename-out [stlc:#%app #%app] [cons/tc cons]))
+(provide (except-out (all-from-out "stlc+var.rkt") stlc:#%app))
 (provide nil isnil head tail)
 
 ;; Simply-Typed Lambda Calculus, plus cons
@@ -13,20 +12,9 @@
 ;; - List constructor
 ;; Terms:
 ;; - terms from stlc+var.rkt
-;; - define, constants only
 
 ;; TODO: enable HO use of list primitives
 
-;; constants only
-(define-syntax (define/tc stx)
-  (syntax-parse stx
-    [(_ x:id e)
-     #:with (e- τ) (infer+erase #'e)
-     #:with y (generate-temporary)
-     #'(begin
-         (define-syntax x (make-rename-transformer (⊢ #'y #'τ)))
-         (define y e-))]))
-
 (define-type-constructor List #:arity 1)
 
 (define-syntax (nil stx)
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
index d100924..d514cd6 100644
--- a/tapl/stlc+var.rkt
+++ b/tapl/stlc+var.rkt
@@ -1,10 +1,11 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?))
-         (except-in "stlc+tup.rkt" #%app λ tup proj let type=?))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?))
+         (except-in "stlc+tup.rkt" #%app begin tup proj let type=?))
+(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
+                     [define/tc define]))
 (provide (except-out (all-from-out "stlc+tup.rkt")
-                     stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj
+                     stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj
                      (for-syntax stlc:type=?)))
 (provide tup proj var case)
 (provide (for-syntax type=?))
@@ -22,6 +23,8 @@
 ;; - terms from stlc+tup.rkt
 ;; - extend tup to include records
 ;; - sums (var)
+;; TopLevel:
+;; - define (values only)
 
 (begin-for-syntax
   ; extend to:
@@ -88,4 +91,12 @@
      (⊢ #'(let ([l_e (car e-)])
             (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
         (stx-car #'(τ_el ...)))]))
-     
\ No newline at end of file
+
+(define-syntax (define/tc stx)
+  (syntax-parse stx
+    [(_ x:id e)
+     #:with (e- τ) (infer+erase #'e)
+     #:with y (generate-temporary)
+     #'(begin
+         (define-syntax x (make-rename-transformer (⊢ #'y #'τ)))
+         (define y e-))]))
\ No newline at end of file