diff --git a/tapl/README.md b/tapl/README.md
index 0b1a435..85f2e88 100644
--- a/tapl/README.md
+++ b/tapl/README.md
@@ -9,11 +9,12 @@ A file extends its immediate parent file.
          - stlc+reco+var.rkt
            - stlc+cons.rkt
              - stlc+box.rkt
-           - stlc+rec-iso.rkt
-           - exist.rkt
+           - exist.rkt (and type=? from stlc+rec-iso)
+         - stlc+rec-iso.rkt (and variants from stlc+reco+var)
      - stlc+sub.rkt
        - stlc+reco+sub.rkt (also pull in tup from stlc+reco+var.rkt)
      - sysf.rkt
-       - fsub.rkt
+       - fsub.rkt (also stlc+reco+sub)
        - fomega.rkt
+         - fomega3.rkt
        - fomega2.rkt
\ No newline at end of file
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
index 8d0d6a2..5150901 100644
--- a/tapl/exist.rkt
+++ b/tapl/exist.rkt
@@ -1,35 +1,29 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "stlc+reco+var.rkt" #%app λ let)
-         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let))
-         (only-in "stlc+rec-iso.rkt")) ; to get current-type=?
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let))
-(provide ∃ pack open)
+(extends "stlc+reco+var.rkt")
+(reuse #:from "stlc+rec-iso.rkt") ; want type=?, but only need to load current-type=?
 
 ;; existential types
-;; combine type=? from sysf (for lam, ie ∃) and stlc+reco+var (for strings)
 ;; Types:
 ;; - types from stlc+reco+var.rkt
 ;; - ∃
 ;; Terms:
 ;; - terms from stlc+reco+var.rkt
 ;; - pack and open
+;; Other: type=? from stlc+rec-iso.rkt
 
 
 (define-type-constructor ∃ #:arity = 1 #:bvs = 1)
 
-(define-syntax (pack stx)
-  (syntax-parse stx
-    [(_ (τ:type e) as ∃τ:type)
-     #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
-     #:with [e- τ_e] (infer+erase #'e)
-     #:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))
-     (⊢ e- : ∃τ.norm)]))
+(define-typed-syntax pack
+  [(_ (τ:type e) as ∃τ:type)
+   #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
+   #:with [e- τ_e] (infer+erase #'e)
+   #:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))
+   (⊢ e- : ∃τ.norm)])
 
-(define-syntax (open stx)
-  (syntax-parse stx #:datum-literals (<=)
-    [(_ ([(tv:id x:id) <= e_packed]) e)
-     #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
+(define-typed-syntax open #:datum-literals (<=)
+  [(_ ([(tv:id x:id) <= e_packed]) e)
+   #:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
      ;; The subst below appears to be a hack, but it's not really.
      ;; It's the (TaPL) type rule itself that is fast and loose.
      ;; Leveraging the macro system's management of binding reveals this.
@@ -73,8 +67,8 @@
      ;; ------------------------------
      ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
      ;;
-     #:with [_ (x-) (e-) (τ_e)]
-            (infer #'(e)
-                   #:tvctx #'([tv : #%type])
-                   #:ctx   #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
-     (⊢ (let ([x- e_packed-]) e-) : τ_e)]))
\ No newline at end of file
+   #:with [_ (x-) (e-) (τ_e)]
+          (infer #'(e)
+                 #:tvctx #'([tv : #%type])
+                 #:ctx   #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
+   (⊢ (let ([x- e_packed-]) e-) : τ_e)])
\ No newline at end of file
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index ddd0888..2b5675f 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -1,17 +1,6 @@
 #lang s-exp "typecheck.rkt"
-;; prefix-in an identifier if:
-;; - it will be extended, eg #%datum
-;; - want to use racket's version in implemetation (this) file, eg #%app
-(require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum))
-         (except-in "stlc+lit.rkt" #%app #%datum))
-(provide (rename-out [datum/tc #%datum]
-                     [stlc:#%app #%app]
-                     [and/tc and] [or/tc or] [if/tc if]
-                     [begin/tc begin]
-                     [let/tc let] [let*/tc let*] [letrec/tc letrec])
-                     ann)
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum)
-         (for-syntax current-join))
+(extends "stlc+lit.rkt" #:except #%datum)
+(provide (for-syntax current-join))
  
 ;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11)
 ;; Types:
@@ -31,11 +20,10 @@
 (define-base-type Bool)
 (define-base-type String)
 
-(define-syntax (datum/tc stx)
-  (syntax-parse stx
-    [(_ . b:boolean) (⊢ (#%datum . b) : Bool)]
-    [(_ . s:str) (⊢ (#%datum . s) : String)]
-    [(_ . x) #'(stlc:#%datum . x)]))
+(define-typed-syntax #%datum
+  [(_ . b:boolean) (⊢ (#%datum . b) : Bool)]
+  [(_ . s:str) (⊢ (#%datum . s) : String)]
+  [(_ . x) #'(stlc+lit:#%datum . x)])
 
 (define-primop zero? : (→ Int Bool))
 (define-primop = : (→ Int Int Bool))
@@ -44,83 +32,76 @@
 (define-primop sub1 : (→ Int Int))
 (define-primop not : (→ Bool Bool))
 
-(define-syntax (and/tc stx)
-  (syntax-parse stx
-    [(_ e1 e2)
-     #:with e1- (⇑ e1 as Bool)
-     #:with e2- (⇑ e2 as Bool)
-     (⊢ (and e1- e2-) : Bool)]))
+(define-typed-syntax and
+  [(_ e1 e2)
+   #:with e1- (⇑ e1 as Bool)
+   #:with e2- (⇑ e2 as Bool)
+   (⊢ (and e1- e2-) : Bool)])
   
-(define-syntax (or/tc stx)
-  (syntax-parse stx
-    [(_ e1 e2)
-     #:with e1- (⇑ e1 as Bool)
-     #:with e2- (⇑ e2 as Bool)
-     (⊢ (or e1- e2-) : Bool)]))
+(define-typed-syntax or
+  [(_ e1 e2)
+   #:with e1- (⇑ e1 as Bool)
+   #:with e2- (⇑ e2 as Bool)
+   (⊢ (or e1- e2-) : Bool)])
 
 (begin-for-syntax 
   (define current-join (make-parameter (λ (x y) x))))
-(define-syntax (if/tc stx)
-  (syntax-parse stx
-    [(_ e_tst e1 e2)
-     #:with e_tst- (⇑ e_tst as Bool)
-     #:with (e1- τ1) (infer+erase #'e1)
-     #:with (e2- τ2) (infer+erase #'e2)
-     #:with τ-out ((current-join) #'τ1 #'τ2)
-     #:fail-unless (and (typecheck? #'τ1 #'τ-out)
-                        (typecheck? #'τ2 #'τ-out))
-                   (format "branches have incompatible types: ~a and ~a"
-                           (type->str #'τ1) (type->str #'τ2))
-     (⊢ (if e_tst- e1- e2-) : τ-out)]))
+(define-typed-syntax if
+  [(_ e_tst e1 e2)
+   #:with e_tst- (⇑ e_tst as Bool)
+   #:with (e1- τ1) (infer+erase #'e1)
+   #:with (e2- τ2) (infer+erase #'e2)
+   #:with τ-out ((current-join) #'τ1 #'τ2)
+   #:fail-unless (and (typecheck? #'τ1 #'τ-out)
+                      (typecheck? #'τ2 #'τ-out))
+                  (format "branches have incompatible types: ~a and ~a"
+                          (type->str #'τ1) (type->str #'τ2))
+   (⊢ (if e_tst- e1- e2-) : τ-out)])
 
 (define-base-type Unit)
 (define-primop void : (→ Unit))
 
-(define-syntax (begin/tc stx)
-  (syntax-parse stx
-    [(_ e_unit ... e)
-     #:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
-     #:with (e- τ) (infer+erase #'e)
-     (⊢ (begin e_unit- ... e-) : τ)]))
+(define-typed-syntax begin
+  [(_ e_unit ... e)
+   #:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
+   #:with (e- τ) (infer+erase #'e)
+   (⊢ (begin e_unit- ... e-) : τ)])
 
-(define-syntax (ann stx)
-  (syntax-parse stx #:datum-literals (:)
-    [(_ e : ascribed-τ:type)
-     #:with (e- τ) (infer+erase #'e)
-     #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
-                   (format "~a does not have type ~a\n"
-                           (syntax->datum #'e) (syntax->datum #'ascribed-τ))
-     (⊢ e- : ascribed-τ)]))
+(define-typed-syntax ann
+  #:datum-literals (:)
+  [(_ e : ascribed-τ:type)
+   #:with (e- τ) (infer+erase #'e)
+   #:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
+                 (format "~a does not have type ~a\n"
+                         (syntax->datum #'e) (syntax->datum #'ascribed-τ))
+   (⊢ e- : ascribed-τ)])
 
-(define-syntax (let/tc stx)
-  (syntax-parse stx
-    [(_ ([x e] ...) e_body)
-     #:with ((e- τ) ...) (infers+erase #'(e ...))
-     #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'e_body)
-     (⊢ (let ([x- e-] ...) e_body-) : τ_body)]))
+(define-typed-syntax let/tc #:export-as let
+  [(_ ([x e] ...) e_body)
+   #:with ((e- τ) ...) (infers+erase #'(e ...))
+   #:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'e_body)
+   (⊢ (let ([x- e-] ...) e_body-) : τ_body)])
 
-(define-syntax (let*/tc stx)
-  (syntax-parse stx
-    [(_ () e_body) #'e_body]
-    [(_ ([x e] [x_rst e_rst] ...) e_body)
-     #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))]))
+(define-typed-syntax let*/tc #:export-as let*
+  [(_ () e_body) #'e_body]
+  [(_ ([x e] [x_rst e_rst] ...) e_body)
+   #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))])
 
-(define-syntax (letrec/tc stx)
-  (syntax-parse stx
-    [(_ ([b:type-bind e] ...) e_body)
-     #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
-            (infers/ctx+erase #'(b ...) #'(e ... e_body))
-     #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
-                   (string-append
-                    "type check fail, args have wrong type:\n"
-                    (string-join
-                     (stx-map
-                      (λ (e τ τ-expect)
-                        (format
-                         "~a has type ~a, expected ~a"
-                         (syntax->datum e) (type->str τ) (type->str τ-expect)))
-                      #'(e ...) #'(τ ...) #'(b.type ...))
-                     "\n"))
-     (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)]))
+(define-typed-syntax letrec
+  [(_ ([b:type-bind e] ...) e_body)
+   #:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
+          (infers/ctx+erase #'(b ...) #'(e ... e_body))
+   #:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
+                 (string-append
+                  "type check fail, args have wrong type:\n"
+                  (string-join
+                   (stx-map
+                    (λ (e τ τ-expect)
+                      (format
+                       "~a has type ~a, expected ~a"
+                       (syntax->datum e) (type->str τ) (type->str τ-expect)))
+                    #'(e ...) #'(τ ...) #'(b.type ...))
+                   "\n"))
+  (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)])
 
      
\ No newline at end of file
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index b814f90..044986a 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -1,38 +1,36 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀)
-         (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀))
-                    [sysf:~∀ ~sysf:∀])
-         (only-in "stlc+reco+var.rkt" String #%datum same-types?))
-(provide (rename-out [sysf:#%app #%app] [sysf:λ λ]))
-(provide (all-from-out "sysf.rkt") (all-from-out "stlc+reco+var.rkt"))
-(provide ∀ inst Λ tyλ tyapp)
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀])
+(reuse String #%datum same-types? #:from "stlc+reco+var.rkt")
 
 ;; System F_omega
 ;; Type relation:
 ;; Types:
 ;; - types from sysf.rkt
+;; - String from stlc+reco+var
 ;; Terms:
-;; - terms from sysf.rkt
+;; - extend ∀ Λ inst from sysf
+;; - add tyλ and tyapp
+;; - #%datum from stlc+reco+var
 
 (define-syntax-category kind)
 
 (begin-for-syntax
   (current-kind? (λ (k) (or (#%type? k) (kind? k))))
-  ;; Try to keep "type?" remain backward compatible with its uses so far,
+  ;; Try to keep "type?" backward compatible with its uses so far,
   ;; eg in the definition of λ or previous type constuctors.
   ;; (However, this is not completely possible, eg define-type-alias)
   ;; So now "type?" no longer validates types, rather it's a subset.
   ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t))
   (current-type? (λ (t) (or (type? t) (★? (typeof t)) (∀★? (typeof t)) #;(kind? (typeof t))))))
 
-; must override
+; must override, to handle kinds
 (provide define-type-alias)
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ)
-     #:with (τ- k_τ) (infer+erase #'τ)
-     #:fail-unless (kind? #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
-     #'(define-syntax alias (syntax-parser [x:id #'τ-]))]))
+     #:with (τ- k_τ) (infer+erase #'τ #:expand (current-type-eval))
+     #:fail-unless ((current-kind?) #'k_τ) (format "not a valid type: ~a\n" (type->str #'τ))
+     #'(define-syntax alias (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))]))
 
 (begin-for-syntax
   (define sysf:type-eval (current-type-eval))
@@ -60,14 +58,13 @@
 (define-kind-constructor ⇒ #:arity >= 1)
 (define-kind-constructor ∀★ #:arity >= 0)
 
-(define-syntax (∀ stx)
-  (syntax-parse stx
-    [(_ bvs:kind-ctx τ_body)
-     ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
-     #:with (tvs- τ_body- k_body)
-            (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
-     ; expand so kind gets overwritten
-     (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
+(define-typed-syntax ∀ #:export-as ∀
+  [(_ bvs:kind-ctx τ_body)
+   ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
+   #:with (tvs- τ_body- k_body)
+          (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+   ; expand so kind gets overwritten
+   (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))])
 (begin-for-syntax
   (define-syntax ~∀
     (pattern-expander
@@ -106,53 +103,49 @@
   (current-type=? type=?)
   (current-typecheck-relation (current-type=?)))
 
-(define-syntax (Λ stx)
-  (syntax-parse stx
-    [(_ bvs:kind-ctx e)
-     #:with ((tv- ...) e- τ_e)
-            (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
-     (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
+(define-typed-syntax Λ
+  [(_ bvs:kind-ctx e)
+   #:with ((tv- ...) e- τ_e)
+          (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+   (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
 
-(define-syntax (inst stx)
-  (syntax-parse stx
-    [(_ e τ ...)
-     #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
-     #:with ([τ- k_τ] ...)
-            (infers+erase #'(τ ...) #:expand (current-type-eval))
-     #:when (stx-andmap
-             (λ (t k) (or ((current-kind?) k)
-                          (type-error #:src t #:msg "not a valid type: ~a" t)))
-             #'(τ ...) #'(k_τ ...))
-     #:when (typechecks? #'(k_τ ...) #'(k ...))
-     (⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))]))
+(define-typed-syntax inst
+  [(_ e τ ...)
+   #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
+   #:with ([τ- k_τ] ...)
+          (infers+erase #'(τ ...) #:expand (current-type-eval))
+   #:when (stx-andmap
+           (λ (t k) (or ((current-kind?) k)
+                        (type-error #:src t #:msg "not a valid type: ~a" t)))
+           #'(τ ...) #'(k_τ ...))
+   #:when (typechecks? #'(k_τ ...) #'(k ...))
+   (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))])
 
 ;; TODO: merge with regular λ and app?
 ;; - see fomega2.rkt
-(define-syntax (tyλ stx)
-  (syntax-parse stx 
-    [(_ bvs:kind-ctx τ_body)
-     #:with (tvs- τ_body- k_body)
-            (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
-     #:when ((current-kind?) #'k_body)
-     (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))]))
+(define-typed-syntax tyλ
+  [(_ bvs:kind-ctx τ_body)
+   #:with (tvs- τ_body- k_body)
+          (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+   #:when ((current-kind?) #'k_body)
+   (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
 
-(define-syntax (tyapp stx)
-  (syntax-parse stx
-    [(_ τ_fn τ_arg ...)
-     #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
-     #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
-     #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
-                   (string-append
-                    (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
-                            (syntax-source stx) (syntax-line stx) (syntax-column stx)
-                            (syntax->datum #'τ_fn))
-                    "or wrong number of arguments:\nGiven:\n"
-                    (string-join
-                     (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
-                          (syntax->datum #'(τ_arg ...))
-                          (stx-map type->str #'(k_arg ...)))
-                     "\n" #:after-last "\n")
-                    (format "Expected: ~a arguments with type(s): "
-                            (stx-length #'(k_in ...)))
-                    (string-join (stx-map type->str #'(k_in ...)) ", "))
-     (⊢ (#%app τ_fn- τ_arg- ...) : k_out)]))
\ No newline at end of file
+(define-typed-syntax tyapp #:export-as tyapp
+  [(_ τ_fn τ_arg ...)
+   #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
+   #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:expand (current-type-eval))
+   #:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
+                 (string-append
+                  (format "~a (~a:~a) Arguments to function ~a have wrong kinds(s), "
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'τ_fn))
+                  "or wrong number of arguments:\nGiven:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(τ_arg ...))
+                        (stx-map type->str #'(k_arg ...)))
+                   "\n" #:after-last "\n")
+                  (format "Expected: ~a arguments with type(s): "
+                          (stx-length #'(k_in ...)))
+                  (string-join (stx-map type->str #'(k_in ...)) ", "))
+   (⊢ (#%app τ_fn- τ_arg- ...) : k_out)])
\ No newline at end of file
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
index 6552499..6de8cbd 100644
--- a/tapl/fomega2.rkt
+++ b/tapl/fomega2.rkt
@@ -1,27 +1,25 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀)
-         (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀))
-                    [sysf:~∀ ~sysf:∀])
-         (only-in "stlc+reco+var.rkt" String #%datum same-types?))
-(provide (rename-out [sysf:#%app #%app] [sysf:λ λ]))
-(provide (all-from-out "sysf.rkt") (all-from-out "stlc+reco+var.rkt"))
-(provide ∀ inst Λ)
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst #:rename [~∀ ~sysf:∀])
+(reuse String #%datum same-types? #:from "stlc+reco+var.rkt")
 
-; same as fomega except here λ and #%app works as both regular and type versions
-;; uses definition from stlc, but tweaks type? and kind? predicates
+; same as fomega.rkt except here λ and #%app works as both type and terms
+; - uses definition from stlc, but tweaks type? and kind? predicates
+;; → is also both type and kind
 
 ;; System F_omega
 ;; Type relation:
 ;; Types:
 ;; - types from sysf.rkt
+;; - String from stlc+reco+var
 ;; Terms:
-;; - terms from sysf.rkt
+;; - extend ∀ Λ inst from sysf
+;; - #%datum from stlc+reco+var
 
 (define-syntax-category kind)
 
 (begin-for-syntax
   (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
-  ;; Try to keep "type?" remain backward compatible with its uses so far,
+  ;; Try to keep "type?" backward compatible with its uses so far,
   ;; eg in the definition of λ or previous type constuctors.
   ;; (However, this is not completely possible, eg define-type-alias)
   ;; So now "type?" no longer validates types, rather it's a subset.
@@ -60,16 +58,14 @@
   (current-type-eval type-eval))
 
 (define-base-kind ★)
-(define-kind-constructor ⇒ #:arity >= 1)
 (define-kind-constructor ∀★ #:arity >= 0)
 
-(define-syntax (∀ stx)
-  (syntax-parse stx
-    [(_ bvs:kind-ctx τ_body)
-     ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
-     #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
-     ; expand so kind gets overwritten
-     (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))]))
+(define-typed-syntax ∀ #:export-as ∀
+  [(_ bvs:kind-ctx τ_body)
+   ;; cant re-use the expansion in sysf:∀ because it will give the bvs kind #%type
+   #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:expand (current-type-eval))
+   ; expand so kind gets overwritten
+   (⊢ #,((current-type-eval) #'(sysf:∀ tvs- τ_body-)) : (∀★ bvs.kind ...))])
 (begin-for-syntax
   (define-syntax ~∀
     (pattern-expander
@@ -108,20 +104,18 @@
   (current-type=? type=?)
   (current-typecheck-relation (current-type=?)))
 
-(define-syntax (Λ stx)
-  (syntax-parse stx
-    [(_ bvs:kind-ctx e)
-     #:with ((tv- ...) e- τ_e)
-            (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
-     (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))]))
+(define-typed-syntax Λ
+  [(_ bvs:kind-ctx e)
+   #:with ((tv- ...) e- τ_e)
+          (infer/ctx+erase #'bvs #'e #:expand (current-type-eval))
+   (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
 
-(define-syntax (inst stx)
-  (syntax-parse stx
-    [(_ e τ ...)
-     #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
-     #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
-     #:when (stx-andmap (λ (t k) (or ((current-kind?) k)
-                                     (type-error #:src t #:msg "not a valid type: ~a" t)))
-                        #'(τ ...) #'(k_τ ...))
-     #:when (typechecks? #'(k_τ ...) #'(k ...))
-     (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))]))
\ No newline at end of file
+(define-typed-syntax inst
+  [(_ e τ ...)
+   #:with (e- (([tv k] ...) τ_body)) (⇑ e as ∀)
+   #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:expand (current-type-eval))
+   #:when (stx-andmap (λ (t k) (or ((current-kind?) k)
+                                   (type-error #:src t #:msg "not a valid type: ~a" t)))
+                      #'(τ ...) #'(k_τ ...))
+   #:when (typechecks? #'(k_τ ...) #'(k ...))
+   (⊢ e- : #,((current-type-eval) (substs #'(τ- ...) #'(tv ...) #'τ_body)))])
\ No newline at end of file
diff --git a/tapl/fomega3.rkt b/tapl/fomega3.rkt
new file mode 100644
index 0000000..1ed6a8e
--- /dev/null
+++ b/tapl/fomega3.rkt
@@ -0,0 +1,53 @@
+#lang s-exp "typecheck.rkt"
+(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
+(reuse String #%datum same-types? #:from "stlc+reco+var.rkt")
+(reuse current-kind? ∀★ ∀★? ★ ★? kind? ∀ Λ inst define-type-alias #:from "fomega.rkt")
+
+; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
+; → is both type and kind --- but reuses parts of fomega.rkt,
+; ie removes the duplication in fomega2.rkt
+
+;; System F_omega
+;; Type relation:
+;; - redefine current-kind? and current-type so #%app and λ
+;;   work for both terms and types
+;; Types:
+;; - types from fomega.rkt
+;; - String from stlc+reco+var
+;; Terms:
+;; - extend ∀ Λ inst from fomega.rkt
+;; - #%datum from stlc+reco+var
+
+;; types and kinds are now mixed, due to #%app and λ
+(begin-for-syntax
+  (current-kind? (λ (k) (or (#%type? k) (kind? k) (#%type? (typeof k)))))
+  ;; Try to keep "type?" backward compatible with its uses so far,
+  ;; eg in the definition of λ or previous type constuctors.
+  ;; (However, this is not completely possible, eg define-type-alias)
+  ;; So now "type?" no longer validates types, rather it's a subset.
+  ;; But we no longer need type? to validate types, instead we can use (kind? (typeof t))
+  (current-type? (λ (t) (or (type? t)
+                            (let ([k (typeof t)])
+                              (or (★? k) (∀★? k)))
+                            ((current-kind?) t)))))
+
+;; extend to handle #%app and λ used as both terms and types
+(begin-for-syntax
+  (define sysf:type-eval (current-type-eval))
+  ;; extend type-eval to handle tyapp
+  ;; - requires manually handling all other forms
+  (define (type-eval τ)
+    (beta (sysf:type-eval τ)))
+  (define (beta τ)
+    (syntax-parse τ
+      [((~literal #%plain-app) τ_fn τ_arg ...)
+       #:with ((~literal #%plain-lambda) (tv ...) τ_body) #'τ_fn
+       ((current-type-eval) (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
+      [((~literal #%plain-lambda) (x ...) τ_body ...)
+       #:with (τ_body+ ...) (stx-map beta #'(τ_body ...))
+       (syntax-track-origin #'(#%plain-lambda (x ...) τ_body+ ...) τ #'#%plain-lambda)]
+      [((~literal #%plain-app) arg ...)
+       #:with (arg+ ...) (stx-map beta #'(arg ...))
+       (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
+      [_ τ]))
+  (current-type-eval type-eval))
\ No newline at end of file
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
index 5a70d2a..271312d 100644
--- a/tapl/fsub.rkt
+++ b/tapl/fsub.rkt
@@ -1,21 +1,15 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "stlc+reco+sub.rkt" #%app λ +)
-         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ))
-         (only-in "sysf.rkt" ∀?)
-         (prefix-in sysf: (only-in "sysf.rkt" ∀))
-         (rename-in (only-in "sysf.rkt" ~∀) [~∀ ~sysf:∀]))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+reco+sub.rkt") stlc:#%app stlc:λ)
-         (except-out (all-from-out "sysf.rkt") sysf:∀ (for-syntax ~sysf:∀)))
-(provide ∀ Λ inst)
+(extends "stlc+reco+sub.rkt" #:except +)
+(reuse ∀? [∀ sysf:∀] [~∀ ~sysf:∀] #:from "sysf.rkt")
  
 ;; System F<:
 ;; Types:
-;; - types from sysf.rkt
+;; - types from sysf.rkt and stlc+reco+sub
 ;; - extend ∀ with bounds
 ;; Terms:
-;; - terms from sysf.rkt
+;; - terms from sysf.rkt and stlc+reco+sub
 ;; - extend Λ and inst
+;; - redefine + with Nat
 ;; Other
 ;; - current-promote, expose
 ;; - extend current-sub? to call current-promote
@@ -50,11 +44,10 @@
 ;; 2) instantiation of ∀
 ;; Problem: need type annotations, even in expanded form
 ;; Solution: store type annotations in a (quasi) kind <:
-(define-syntax ∀
-  (syntax-parser #:datum-literals (<:)
-    [(_ ([tv:id <: τ:type] ...) τ_body)
-     ; eval first to overwrite the old #%type
-     (⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))]))
+(define-typed-syntax ∀ #:export-as ∀ #:datum-literals (<:)
+  [(_ ([tv:id <: τ:type] ...) τ_body)
+   ; eval first to overwrite the old #%type
+   (⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))])
 (begin-for-syntax
   (define-syntax ~∀
     (pattern-expander
@@ -79,20 +72,18 @@
                        #:src #'any
                        #:msg "Expected ∀ type, got: ~a" #'any))))]))))
 
-(define-syntax (Λ stx)
-  (syntax-parse stx #:datum-literals (<:)
-    [(_ ([tv:id <: τsub:type] ...) e)
-     ;; NOTE: store the subtyping relation of tv and τsub in another
-     ;; "environment", ie, a syntax property with another tag: 'sub
-     ;; The "expose" function looks for this tag to enforce the bound,
-     ;; as in TaPL (fig 28-1)
-     #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
-                                                  #:octx  #'([tv : τsub] ...) #:tag 'sub)
-     (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))]))
-(define-syntax (inst stx)
-  (syntax-parse stx
-    [(_ e τ:type ...)
-     #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
-     #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
-     (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
+(define-typed-syntax Λ #:datum-literals (<:)
+  [(_ ([tv:id <: τsub:type] ...) e)
+   ;; NOTE: store the subtyping relation of tv and τsub in another
+   ;; "environment", ie, a syntax property with another tag: 'sub
+   ;; The "expose" function looks for this tag to enforce the bound,
+   ;; as in TaPL (fig 28-1)
+   #:with ((tv- ...) _ (e-) (τ_e)) (infer #'(e) #:tvctx #'([tv : #%type] ...)
+                                                #:octx  #'([tv : τsub] ...) #:tag 'sub)
+   (⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))])
+(define-typed-syntax inst
+  [(_ e τ:type ...)
+   #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
+   #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
+   (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))])
 
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
index 46dc8fb..f5e9cd4 100644
--- a/tapl/stlc+box.rkt
+++ b/tapl/stlc+box.rkt
@@ -1,9 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(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 :=)
+(extends "stlc+cons.rkt")
 
 ;; Simply-Typed Lambda Calculus, plus mutable references
 ;; Types:
@@ -11,23 +7,21 @@
 ;; - Ref constructor
 ;; Terms:
 ;; - terms from stlc+cons.rkt
+;; - ref deref :=
 
 (define-type-constructor Ref #:arity = 1)
 
-(define-syntax (ref stx)
-  (syntax-parse stx
-    [(_ e)
-     #:with (e- τ) (infer+erase #'e)
-     (⊢ (box e-) : (Ref τ))]))
-(define-syntax (deref stx)
-  (syntax-parse stx
-    [(_ e)
-     #:with (e- (τ)) (⇑ e as Ref)
-     (⊢ (unbox e-) : τ)]))
-(define-syntax (:= stx)
-  (syntax-parse stx
-    [(_ e_ref e)
-     #:with (e_ref- (τ1)) (⇑ e_ref as Ref)
-     #:with (e- τ2) (infer+erase #'e)
-     #:when (typecheck? #'τ1 #'τ2)
-     (⊢ (set-box! e_ref- e-) : Unit)]))
\ No newline at end of file
+(define-typed-syntax ref
+  [(_ e)
+   #:with (e- τ) (infer+erase #'e)
+   (⊢ (box e-) : (Ref τ))])
+(define-typed-syntax deref
+  [(_ e)
+   #:with (e- (τ)) (⇑ e as Ref)
+   (⊢ (unbox e-) : τ)])
+(define-typed-syntax :=
+  [(_ e_ref e)
+   #:with (e_ref- (τ1)) (⇑ e_ref as Ref)
+   #:with (e- τ2) (infer+erase #'e)
+   #:when (typecheck? #'τ1 #'τ2)
+   (⊢ (set-box! e_ref- e-) : Unit)])
\ No newline at end of file
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 54fe74d..16e5318 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -1,9 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app))
-         (except-in "stlc+reco+var.rkt" #%app))
-(provide (rename-out [stlc:#%app #%app] [cons/tc cons]))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app))
-(provide nil isnil head tail)
+(extends "stlc+reco+var.rkt")
 
 ;; Simply-Typed Lambda Calculus, plus cons
 ;; Types:
@@ -16,33 +12,25 @@
 
 (define-type-constructor List #:arity = 1)
 
-(define-syntax (nil stx)
-  (syntax-parse stx
-    [(_ ~! τi:type-ann)
-     (⊢ null : (List τi.norm))]
-    [null:id
-     #:fail-when #t (error 'nil "requires type annotation")
-     #'null]))
-(define-syntax (cons/tc stx)
-  (syntax-parse stx
-    [(_ e1 e2)
-     #:with (e1- τ1) (infer+erase #'e1)
-     #:with (e2- (τ2)) (⇑ e2 as List)
-     #:when (typecheck? #'τ1 #'τ2)
-     (⊢ (cons e1- e2-) : (List τ1))]))
-(define-syntax (isnil stx)
-  (syntax-parse stx
-    [(_ e)
-     #:with (e- _) (⇑ e as List)
-     (⊢ (null? e-) : Bool)]))
-(define-syntax (head stx)
-  (syntax-parse stx
-    [(_ e)
-     #:with (e- (τ)) (⇑ e as List)
-     (⊢ (car e-) : τ)]))
-(define-syntax (tail stx)
-  (syntax-parse stx
-    [(_ e)
-     #:with (e- τ-lst) (infer+erase #'e)
-     #:when (List? #'τ-lst)
-     (⊢ (cdr e-) : τ-lst)]))
\ No newline at end of file
+(define-typed-syntax nil
+  [(_ ~! τi:type-ann) (⊢ null : (List τi.norm))]
+  [_:id #:fail-when #t (error 'nil "requires type annotation") #'(void)])
+(define-typed-syntax cons
+  [(_ e1 e2)
+   #:with (e1- τ1) (infer+erase #'e1)
+   #:with (e2- (τ2)) (⇑ e2 as List)
+   #:when (typecheck? #'τ1 #'τ2)
+   (⊢ (cons e1- e2-) : (List τ1))])
+(define-typed-syntax isnil
+  [(_ e)
+   #:with (e- _) (⇑ e as List)
+   (⊢ (null? e-) : Bool)])
+(define-typed-syntax head
+  [(_ e)
+   #:with (e- (τ)) (⇑ e as List)
+   (⊢ (car e-) : τ)])
+(define-typed-syntax tail
+  [(_ e)
+   #:with (e- τ-lst) (infer+erase #'e)
+   #:when (List? #'τ-lst)
+   (⊢ (cdr e-) : τ-lst)])
\ No newline at end of file
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
index d574e4f..d2851f4 100644
--- a/tapl/stlc+lit.rkt
+++ b/tapl/stlc+lit.rkt
@@ -1,10 +1,6 @@
 #lang s-exp "typecheck.rkt"
-;(extends "stlc.rkt" #:impl-uses (→))
-(require (except-in "stlc.rkt" #%app)
-         (prefix-in stlc: (only-in "stlc.rkt" #%app)))
-(provide (except-out (all-from-out "stlc.rkt") stlc:#%app))
-(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum])
-         define-primop)
+(extends "stlc.rkt")
+(provide define-primop)
  
 ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
 ;; Types:
@@ -33,9 +29,8 @@
 
 (define-primop + : (→ Int Int Int))
 
-(define-syntax (datum/tc stx)
-  (syntax-parse stx
-    [(_ . n:integer) (⊢ (#%datum . n) : Int)]
-    [(_ . x)
-     #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
-     #'(#%datum . x)]))
+(define-typed-syntax #%datum
+  [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+  [(_ . x)
+   #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
+   #'(#%datum . x)])
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
index 2ba483c..dff2dad 100644
--- a/tapl/stlc+rec-iso.rkt
+++ b/tapl/stlc+rec-iso.rkt
@@ -1,19 +1,18 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "stlc+tup.rkt" #%app λ) ; import tuples, not records
-         (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ))
-         (only-in "stlc+reco+var.rkt" ∨ var case define-type-alias define)) ; and variants
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+tup.rkt") stlc:#%app stlc:λ)
-         (all-from-out "stlc+reco+var.rkt"))
-(provide μ fld unfld)
+(extends "stlc+tup.rkt")
+(reuse ∨ var case define-type-alias define #:from "stlc+reco+var.rkt")
 
 ;; stlc + (iso) recursive types
 ;; Types:
-;; - types from stlc+reco+var.rkt
+;; - types from stlc+tup.rkt
+;; - also ∨ from stlc+reco+var
 ;; - μ
 ;; Terms:
-;; - terms from stlc+reco+var.rkt
-;; - fld/unfld
+;; - terms from stlc+tup.rkt
+;; - also var and case from stlc+reco+var
+;; - fld, unfld
+;; Other:
+;; - extend type=? to handle lambdas
 
 (define-type-constructor μ #:arity = 1 #:bvs = 1)
 
@@ -24,9 +23,7 @@
 ;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
 ;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
     (syntax-parse (list τ1 τ2)
-      [#;(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
-        ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
-       (((~literal #%plain-app) tycon1 ((~literal #%plain-lambda) (x:id ...) k1 ... t1))
+      [(((~literal #%plain-app) tycon1 ((~literal #%plain-lambda) (x:id ...) k1 ... t1))
         ((~literal #%plain-app) tycon2 ((~literal #%plain-lambda) (y:id ...) k2 ... t2)))
        #:when ((current-type=?) #'tycon1 #'tycon2)
        #:when (types=? #'(k1 ...) #'(k2 ...))
@@ -38,17 +35,15 @@
   (current-type=? type=?)
   (current-typecheck-relation type=?))
 
-(define-syntax (unfld stx)
-  (syntax-parse stx
-    [(_ τ:type-ann e)
-     #:with (~μ* (tv) τ_body) #'τ.norm
-     #:with [e- τ_e] (infer+erase #'e)
-     #:when (typecheck? #'τ_e #'τ.norm)
-     (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))]))
-(define-syntax (fld stx)
-  (syntax-parse stx
-    [(_ τ:type-ann e)
-     #:with (~μ* (tv) τ_body) #'τ.norm
-     #:with [e- τ_e] (infer+erase #'e)
-     #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
-     (⊢ e- : τ.norm)]))
\ No newline at end of file
+(define-typed-syntax unfld
+  [(_ τ:type-ann e)
+   #:with (~μ* (tv) τ_body) #'τ.norm
+   #:with [e- τ_e] (infer+erase #'e)
+   #:when (typecheck? #'τ_e #'τ.norm)
+   (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))])
+(define-typed-syntax fld
+  [(_ τ:type-ann e)
+   #:with (~μ* (tv) τ_body) #'τ.norm
+   #:with [e- τ_e] (infer+erase #'e)
+   #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
+   (⊢ e- : τ.norm)])
\ No newline at end of file
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
index 9aa79cd..d0c5074 100644
--- a/tapl/stlc+reco+sub.rkt
+++ b/tapl/stlc+reco+sub.rkt
@@ -1,14 +1,8 @@
 #lang s-exp "typecheck.rkt"
+(extends "stlc+sub.rkt" #:except #%app #%datum)
+(extends "stlc+reco+var.rkt" #:except #%datum +)
 ;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
 ;; but extend sub? from stlc+sub.rkt
-(require (except-in "stlc+sub.rkt" #%app #%datum)
-         (prefix-in stlc+sub: (only-in "stlc+sub.rkt" #%app #%datum))
-         (except-in "stlc+reco+var.rkt" #%app #%datum +)
-         (prefix-in stlc+reco+var: (only-in "stlc+reco+var.rkt" #%datum)))
-(provide (rename-out [stlc+sub:#%app #%app]
-                     [datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+sub.rkt") stlc+sub:#%app stlc+sub:#%datum)
-         (except-out (all-from-out "stlc+reco+var.rkt") stlc+reco+var:#%datum))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping, plus records
 ;; Types:
@@ -16,12 +10,12 @@
 ;; Type relations:
 ;; - sub? extended to records
 ;; Terms:
-;; - terms from stlc+sub.rkt, can leave record form as is
+;; - terms from stlc+sub.rkt
+;; - records and variants from stlc+reco+var
 
-(define-syntax (datum/tc stx)
-  (syntax-parse stx
-    [(_ . n:number) #'(stlc+sub:#%datum . n)]
-    [(_ . x) #'(stlc+reco+var:#%datum . x)]))
+(define-typed-syntax #%datum
+  [(_ . n:number) #'(stlc+sub:#%datum . n)]
+  [(_ . x) #'(stlc+reco+var:#%datum . x)])
 
 (begin-for-syntax
   (define old-sub? (current-sub?))
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
index 8415d3c..bf8ff05 100644
--- a/tapl/stlc+reco+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -1,15 +1,7 @@
 #lang s-exp "typecheck.rkt"
-(require (only-in racket/bool symbol=?))
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let × ×?))
-         (except-in "stlc+tup.rkt" #%app begin tup proj let ×)
-         (rename-in (only-in "stlc+tup.rkt" ~×) [~× ~stlc:×]))
-(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:let stlc:begin stlc:×
-                     (for-syntax ~stlc:× stlc:×?)))
-(provide × tup proj ∨ var case)
-(provide (for-syntax same-types? ~× ~×* ~∨ ~∨*))
+(extends "stlc+tup.rkt" #:except × ×? tup proj
+                        #:rename [~× ~stlc:×])
+(provide × ∨ (for-syntax same-types? ~× ~×* ~∨ ~∨*))
 
 
 ;; Simply-Typed Lambda Calculus, plus records and variants
@@ -39,14 +31,13 @@
     [(_ alias:id τ:type)
      #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
 
-(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-typed-syntax define
+  [(_ x:id e)
+   #:with (e- τ) (infer+erase #'e)
+   #:with y (generate-temporary)
+   #'(begin
+       (define-syntax x (make-rename-transformer (⊢ y : τ)))
+       (define y e-))])
 
 ; re-define tuples as records
 ; dont use define-type-constructor because I want the : literal syntax
@@ -54,7 +45,7 @@
   (syntax-parser #:datum-literals (:)
     [(_ [label:id : τ:type] ...)
      #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...))
-     #`(stlc:× valid-τ ...)]))
+     #`(stlc+tup:× valid-τ ...)]))
 (begin-for-syntax
   (define-syntax ~×
     (pattern-expander
@@ -64,7 +55,7 @@
        [(_ . args)
         #'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...))
                 (~parse args #'((l τ_l) (... ...))))])))
-  (define ×? stlc:×?)
+  (define ×? stlc+tup:×?)
   (define-syntax ~×*
     (pattern-expander
      (syntax-parser #:datum-literals (:)
@@ -75,21 +66,19 @@
                                #:msg "Expected × type, got: ~a" #'any))))]))))
 
 ;; records
-(define-syntax (tup stx)
-  (syntax-parse stx #:datum-literals (=)
-    [(_ [l:id = e] ...)
-     #:with ([e- τ] ...) (infers+erase #'(e ...))
-     (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))]))
-(define-syntax (proj stx)
-  (syntax-parse stx #:literals (quote)
-    [(_ e_rec l:id)
-     #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
-     #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
-     (⊢ (cadr (assoc 'l e_rec-)) : τ_match)]))
+(define-typed-syntax tup #:datum-literals (=)
+  [(_ [l:id = e] ...)
+   #:with ([e- τ] ...) (infers+erase #'(e ...))
+   (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))])
+(define-typed-syntax proj #:literals (quote)
+  [(_ e_rec l:id)
+   #:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
+   #:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
+   (⊢ (cadr (assoc 'l e_rec-)) : τ_match)])
 
 (define-type-constructor ∨/internal)
 
-; re-define tuples as records
+;; variants
 (define-syntax ∨
   (syntax-parser #:datum-literals (:)
     [(_ (~and [label:id : τ:type] x) ...)
@@ -122,27 +111,26 @@
                                     #:msg "Expected ∨ type, got: ~a" #'any))))
                ~!)])))) ; dont backtrack here
 
-(define-syntax (var stx)
-  (syntax-parse stx #:datum-literals (as =)
-    [(_ l:id = e as τ:type)
-     #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
-     #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
-     #:fail-unless (syntax-e #'match_res)
-                   (format "~a field does not exist" (syntax->datum #'l))
-     #:with (_ τ_match) #'match_res
-     #:with (e- τ_e) (infer+erase #'e)
-     #:when (typecheck? #'τ_e #'τ_match)
-     (⊢ (list 'l e) : τ)]))
-(define-syntax (case stx)
-  (syntax-parse stx #:datum-literals (of =>)
-    [(_ e [l:id x:id => e_l] ...)
-     #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
-     #:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
-     #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
-     #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
-     #:with (((x-) e_l- τ_el) ...)
-            (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
-     #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
-     (⊢ (let ([l_e (car e-)])
-          (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
-        : #,(stx-car #'(τ_el ...)))]))
+(define-typed-syntax var #:datum-literals (as =)
+  [(_ l:id = e as τ:type)
+   #:with (~∨* [l_τ : τ_l] ...) #'τ.norm
+   #:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
+   #:fail-unless (syntax-e #'match_res)
+                 (format "~a field does not exist" (syntax->datum #'l))
+   #:with (_ τ_match) #'match_res
+   #:with (e- τ_e) (infer+erase #'e)
+   #:when (typecheck? #'τ_e #'τ_match)
+   (⊢ (list 'l e) : τ)])
+(define-typed-syntax case
+  #:datum-literals (of =>)
+  [(_ e [l:id x:id => e_l] ...)
+   #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+   #:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
+   #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
+   #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
+   #:with (((x-) e_l- τ_el) ...)
+          (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+   #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
+   (⊢ (let ([l_e (car e-)])
+        (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
+      : #,(stx-car #'(τ_el ...)))])
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
index 620bdd7..68b32b3 100644
--- a/tapl/stlc+sub.rkt
+++ b/tapl/stlc+sub.rkt
@@ -1,8 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "stlc+lit.rkt" #%datum + #%app)
-         (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)))
-(provide (rename-out [stlc:#%app #%app] [datum/tc #%datum]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:#%datum))
+(extends "stlc+lit.rkt" #:except #%datum +)
 (provide (for-syntax subs? current-sub?))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping
@@ -16,7 +13,9 @@
 ;;   - Int <: Num
 ;;   - →
 ;; Terms:
-;; - terms from stlc+lit.rkt, except redefined: app, datum, +
+;; - terms from stlc+lit.rkt, except redefined: datum and +
+;; - also *
+;; Other: sub? current-sub?
 
 (define-base-type Top)
 (define-base-type Num)
@@ -25,12 +24,11 @@
 (define-primop + : (→ Num Num Num))
 (define-primop * : (→ Num Num Num))
 
-(define-syntax (datum/tc stx)
-  (syntax-parse stx
-    [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
-    [(_ . n:integer) (⊢ (#%datum . n) : Int)]
-    [(_ . n:number) (⊢ (#%datum . n) : Num)]
-    [(_ . x) #'(stlc:#%datum . x)]))
+(define-typed-syntax #%datum
+  [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
+  [(_ . n:integer) (⊢ (#%datum . n) : Int)]
+  [(_ . n:number) (⊢ (#%datum . n) : Num)]
+  [(_ . x) #'(stlc+lit:#%datum . x)])
 
 (begin-for-syntax
   (define (sub? t1 t2)
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
index 2693cb7..c0d6eaf 100644
--- a/tapl/stlc+tup.rkt
+++ b/tapl/stlc+tup.rkt
@@ -1,9 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app))
-         (except-in "ext-stlc.rkt" #%app))
-(provide (rename-out [stlc:#%app #%app])
-         tup proj)
-(provide (except-out (all-from-out "ext-stlc.rkt") stlc:#%app))
+(extends "ext-stlc.rkt")
  
 ;; Simply-Typed Lambda Calculus, plus tuples
 ;; Types:
@@ -15,15 +11,13 @@
 
 (define-type-constructor ×) ; default arity >=0
 
-(define-syntax (tup stx)
-  (syntax-parse stx
-    [(_ e ...)
-     #:with ([e- τ] ...) (infers+erase #'(e ...))
-     (⊢ (list e- ...) : (× τ ...))]))
-(define-syntax (proj stx)
-  (syntax-parse stx
-    [(_ e_tup n:nat)
-     #:with [e_tup- τs_tup] (⇑ e_tup as ×)
-     #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
-     (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]))
+(define-typed-syntax tup
+  [(_ e ...)
+   #:with ([e- τ] ...) (infers+erase #'(e ...))
+   (⊢ (list e- ...) : (× τ ...))])
+(define-typed-syntax proj
+  [(_ e_tup n:nat)
+   #:with [e_tup- τs_tup] (⇑ e_tup as ×)
+   #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
+   (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
    
\ No newline at end of file
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
index 4312c1c..e248afd 100644
--- a/tapl/stlc.rkt
+++ b/tapl/stlc.rkt
@@ -1,7 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(provide (rename-out [λ/tc λ] [app/tc #%app]))
 (provide (for-syntax current-type=? types=?))
-(provide #%module-begin #%top-interaction #%top require) ; useful racket forms
  
 ;; Simply-Typed Lambda Calculus
 ;; - no base types; can't write any terms
@@ -66,29 +64,27 @@
 
 (define-type-constructor → #:arity >= 1)
 
-(define-syntax (λ/tc stx)
-  (syntax-parse stx 
-    [(_ bvs:type-ctx e)
-     #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
-     (⊢ (λ xs- e-) : (→ bvs.type ... τ_res))]))
+(define-typed-syntax λ
+  [(_ bvs:type-ctx e)
+   #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
+   (⊢ (λ xs- e-) : (→ bvs.type ... τ_res))])
 
-(define-syntax (app/tc stx)
-  (syntax-parse stx
-    [(_ e_fn e_arg ...)
-     #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
-     #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
-     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
-                   (string-append
-                    (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
-                            (syntax-source stx) (syntax-line stx) (syntax-column stx)
-                            (syntax->datum #'e_fn))
-                    "or wrong number of arguments:\nGiven:\n"
-                    (string-join
-                     (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
-                          (syntax->datum #'(e_arg ...))
-                          (stx-map type->str #'(τ_arg ...)))
-                     "\n" #:after-last "\n")
-                    (format "Expected: ~a arguments with type(s): "
-                            (stx-length #'(τ_in ...)))
-                    (string-join (stx-map type->str #'(τ_in ...)) ", "))
-     (⊢ (#%app e_fn- e_arg- ...) : τ_out)]))
+(define-typed-syntax #%app
+  [(_ e_fn e_arg ...)
+   #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
+   #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+   #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+                 (string-append
+                  (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
+                          (syntax-source stx) (syntax-line stx) (syntax-column stx)
+                          (syntax->datum #'e_fn))
+                  "or wrong number of arguments:\nGiven:\n"
+                  (string-join
+                   (map (λ (e t) (format "  ~a : ~a" e t)) ; indent each line
+                        (syntax->datum #'(e_arg ...))
+                        (stx-map type->str #'(τ_arg ...)))
+                   "\n" #:after-last "\n")
+                  (format "Expected: ~a arguments with type(s): "
+                          (stx-length #'(τ_in ...)))
+                  (string-join (stx-map type->str #'(τ_in ...)) ", "))
+  (⊢ (#%app e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
index ab86a99..7177274 100644
--- a/tapl/sysf.rkt
+++ b/tapl/sysf.rkt
@@ -1,11 +1,7 @@
 #lang s-exp "typecheck.rkt"
-(require (except-in "stlc+lit.rkt" #%app λ)
-         (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ))
-         (only-in "stlc+rec-iso.rkt")) ; want type=? from here
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app stlc:λ))
-(provide Λ inst)
- 
+(extends "stlc+lit.rkt")
+(reuse #:from "stlc+rec-iso.rkt") ; want this type=?
+
 ;; System F
 ;; Type relation:
 ;; - extend type=? with ∀
@@ -18,13 +14,11 @@
 
 (define-type-constructor ∀ #:arity = 1 #:bvs >= 0)
 
-(define-syntax (Λ stx)
-  (syntax-parse stx
-    [(_ (tv:id ...) e)
-     #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
-     (⊢ e- : (∀ (tv- ...) τ))]))
-(define-syntax (inst stx)
-  (syntax-parse stx
-    [(_ e τ:type ...)
-     #:with (e- (tvs (τ_body))) (⇑ e as ∀)
-     (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #;#'(tv ...) #'τ_body))]))
\ No newline at end of file
+(define-typed-syntax Λ
+  [(_ (tv:id ...) e)
+   #:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
+   (⊢ e- : (∀ (tv- ...) τ))])
+(define-typed-syntax inst
+  [(_ e τ:type ...)
+   #:with (e- (tvs (τ_body))) (⇑ e as ∀)
+   (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))])
\ No newline at end of file
diff --git a/tapl/tests/fomega3-tests.rkt b/tapl/tests/fomega3-tests.rkt
new file mode 100644
index 0000000..9a98ede
--- /dev/null
+++ b/tapl/tests/fomega3-tests.rkt
@@ -0,0 +1,200 @@
+#lang s-exp "../fomega3.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type Int : ★)
+(check-type String : ★)
+(typecheck-fail →)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
+(typecheck-fail (→ 1))
+(check-type 1 : Int)
+
+;(check-type (∀ ([t : ★]) (→ t t)) : ★)
+(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
+(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
+            : (∀ ([X : ★]) (→ X X)))
+(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
+
+(check-type (λ ([t : ★]) t) : (→ ★ ★))
+(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
+(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
+(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
+(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
+
+(check-type ((λ ([t : ★]) t) Int) : ★)
+(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
+(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
+(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
+
+;; partial-apply →
+(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
+            : (→ ★ ★))
+; f's type must have kind ★
+(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
+(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
+            (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
+(check-type (inst
+             (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+             ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+            : (→ (→ Int String) (→ Int String)))
+(typecheck-fail
+ (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
+ ;#:with-msg "not a valid type: 1")
+
+;; applied f too early
+(typecheck-fail (inst
+                 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
+                 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
+(check-type ((inst
+              (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+             (λ ([x : Int]) "int")) : (→ Int String))
+(check-type (((inst
+               (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
+              ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
+              (λ ([x : Int]) "int")) 1) : String ⇒ "int")
+
+;; tapl examples, p441
+(typecheck-fail
+ (define-type-alias tmp 1))
+ ;#:with-msg "not a valid type: 1")
+(define-type-alias Id (λ ([X : ★]) X))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
+(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
+(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
+
+;; tapl examples, p451
+(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
+
+;(check-type Pair : (→ ★ ★ ★))
+(check-type Pair : (→ ★ ★ (∀★ ★)))
+
+(check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X)))
+; parametric pair constructor
+(check-type
+ (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+ : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y))))
+; concrete Pair Int String constructor
+(check-type
+ (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String)
+ : (→ Int String (Pair Int String)))
+; Pair Int String value
+(check-type
+ ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+       Int String) 1 "1")
+ : (Pair Int String))
+; fst: parametric
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X)))
+; fst: concrete Pair Int String accessor
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+  Int String)
+ : (→ (Pair Int String) Int))
+; apply fst
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : Int ⇒ 1)
+; snd
+(check-type
+ (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+ : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y)))
+(check-type
+ (inst
+  (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+  Int String)
+ : (→ (Pair Int String) String))
+(check-type
+ ((inst
+   (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y))))
+   Int String)
+  ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y)))))
+         Int String) 1 "1"))
+ : String ⇒ "1")
+
+;;; sysf tests wont work, unless augmented with kinds
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false
+(check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+            : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
+; first inst should be discarded
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+; second inst is discarded
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+
+;; polymorphic arguments
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
+(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
+(check-type
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
+(check-type
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
+ : Int ⇒ 10)
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+             (Λ ([s : ★]) (λ ([y : s]) y)))
+             : Int ⇒ 10)
+
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+;(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 911a260..7d83b01 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -24,4 +24,5 @@
 
 ;; F_omega
 (require "fomega-tests.rkt")
-(require "fomega2-tests.rkt")
\ No newline at end of file
+(require "fomega2-tests.rkt")
+(require "fomega3-tests.rkt")
\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 4a940dc..098b052 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -1,14 +1,15 @@
 #lang racket/base
 (require
-  (for-syntax (except-in racket extends)
-              syntax/parse racket/syntax syntax/stx
+  (for-syntax (except-in racket extends) (only-in srfi/13 string-prefix?)
+              syntax/parse racket/syntax syntax/stx racket/stxparam
               "stx-utils.rkt"
               syntax/parse/debug)
   (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
   (for-meta 3 racket/base syntax/parse racket/syntax)
-  racket/provide)
+  racket/bool racket/provide racket/require)
 (provide
- (all-from-out racket/base)
+ symbol=?
+ (except-out (all-from-out racket/base) #%module-begin)
  (for-syntax (all-defined-out)) (all-defined-out)
  (for-syntax
   (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
@@ -27,9 +28,35 @@
 ;;   aliasing, is just free-identifier=?
 ;; - type constructors are prefix
 
+;; redefine #%module-begin to add some provides
+(provide (rename-out [mb #%module-begin]))
+(define-syntax (mb stx)
+  (syntax-parse stx
+    [(_ . stuff)
+     #'(#%module-begin
+        (provide #%module-begin #%top-interaction #%top require) ; useful racket forms
+        . stuff)]))
+
 (struct exn:fail:type:runtime exn:fail:user ())
 
-;; require macro
+(define-for-syntax (drop-file-ext filename)
+  (car (string-split filename ".")))
+
+(begin-for-syntax
+  (define-syntax-parameter stx (syntax-rules ())))
+
+(define-syntax (define-typed-syntax stx)
+  (syntax-parse stx
+    [(_ name:id #:export-as out-name:id stx-parse-clause ...)
+     #'(begin
+         (provide (rename-out [name out-name]))
+         (define-syntax (name syntx)
+           (syntax-parameterize ([stx (syntax-id-rules () [_ syntx])])
+             (syntax-parse syntx stx-parse-clause ...))))]
+    [(_ name:id stx-parse-clause ...)
+     #`(define-typed-syntax #,(generate-temporary) #:export-as name
+         stx-parse-clause ...)]))
+
 ;; need options for
 ;; - pass through
 ;;   - use (generated) prefix to avoid conflicts
@@ -41,19 +68,55 @@
 (define-syntax extends
   (syntax-parser
     [(_ base-lang
-        (~optional (~seq #:impl-uses (x ...)) #:defaults ([(x 1) null])))
-     #:with pre (generate-temporary)
+        (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) #:defaults ([(x 1) null]))
+        (~optional (~seq #:rename [old new] ...) #:defaults ([(old 1) null][(new 1) null]))
+        (~optional (~seq #:prefix p ...) #:defaults ([(p 1) null])))
+     #:with pre (or (let ([dat (syntax-e #'base-lang)])
+                      (and (string? dat)
+                           (string->symbol (drop-file-ext dat))))
+                    #'base-lang)                    
      #:with pre: (format-id #'pre "~a:" #'pre)
-     #'(begin
-         (require (prefix-in pre: base-lang))
-         (require (only-in base-lang x ...))
+     #:with internal-pre (generate-temporary)
+     #:with non-excluded-imports #'(except-in base-lang p ... x ... old ...)
+     #:with conflicted? #'(λ (n) (member (string->symbol n) '(#%app λ #%datum begin let let* letrec if define)))
+     #:with not-conflicted? #'(λ (n) (and (not (conflicted? n)) n))
+     #`(begin
+         (require (prefix-in pre: (only-in base-lang p ... x ...))) ; prefixed
+         (require (rename-in (only-in base-lang old ...) [old new] ...))
+         (require (filtered-in not-conflicted? non-excluded-imports))
+         (require (filtered-in ; conflicted names, with (internal) prefix
+                   (let ([conflicted-pre (symbol->string (syntax->datum #'internal-pre))])
+                     (λ (name) (and (conflicted? name)
+                                    (string-append conflicted-pre name))))
+                   non-excluded-imports))
          (provide (filtered-out
-                   (let ([pre-pat (regexp (format "^~a" (syntax->datum #'pre:)))])
+                   (let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
+                          [int-pre-str #,(symbol->string (syntax->datum #'internal-pre))]
+                          [pre-str-len (string-length pre-str)]
+                          [int-pre-str-len (string-length int-pre-str)]
+                          [drop-pre (λ (s) (substring s pre-str-len))]
+                          [drop-int-pre (λ (s) (substring s int-pre-str-len))]
+                          [excluded (map symbol->string (syntax->datum #'(x ... new ...)))])
                      (λ (name)
-                       (and (regexp-match? pre-pat name)
-                            (regexp-replace pre-pat name ""))))
+                       (define out-name
+                         (or (and (string-prefix? pre-str name)
+                                  (drop-pre name))
+                             (and (string-prefix? int-pre-str name)
+                                  (drop-int-pre name))
+                             name))
+                       (and (not (member out-name excluded)) out-name)))
+                   (all-from-out base-lang))
+                  ))]))
+(define-syntax reuse
+  (syntax-parser
+    [(_ (~or x:id [old:id new:id]) ... #:from base-lang)
+     #`(begin
+         (require (rename-in (only-in base-lang x ... old ...) [old new] ...))
+         (provide (filtered-out
+                   (let ([excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))])
+                     (λ (n) (and (not (member n excluded)) n)))
                    (all-from-out base-lang))))]))
-                 
+
 ;; type assignment
 (begin-for-syntax
   ;; Type assignment macro for nicer syntax
@@ -411,7 +474,7 @@
      #:with define-name-cons (format-id #'name "define-~a-constructor" #'name)
      #:with name-ann (format-id #'name "~a-ann" #'name)
      #'(begin
-         (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann)
+         (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx)
                   #%tag define-base-name define-name-cons)
          (define #%tag void)
          (begin-for-syntax