diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
index 8d4ca01..47c63de 100644
--- a/tapl/fsub.rkt
+++ b/tapl/fsub.rkt
@@ -1,12 +1,128 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app)
-         (prefix-in sysf: (only-in "sysf.rkt" #%app)))
-(provide (rename-out [sysf:#%app #%app]))
-(provide (except-out (all-from-out "sysf.rkt") sysf:#%app))
+(require (except-in "sysf.rkt" #%app #%datum + ∀ Λ inst type=?)
+         (prefix-in sysf: (only-in "sysf.rkt" #%app ∀ Λ inst type=?))
+         (except-in "stlc+reco+sub.rkt" #%app + type=? proj)
+         (prefix-in stlc: (only-in "stlc+reco+sub.rkt" type=? proj)))
+(provide (rename-out [app/tc #%app]))
+(provide (except-out (all-from-out "sysf.rkt")
+                     sysf:#%app sysf:∀ sysf:Λ sysf:inst
+                     (for-syntax sysf:type=?))
+         (except-out (all-from-out "stlc+reco+sub.rkt")
+                     (for-syntax stlc:type=?)))
+(provide ∀ Λ inst proj)
  
 ;; System F<:
 ;; Types:
 ;; - types from sysf.rkt
 ;; Terms:
 ;; - terms from sysf.rkt
+
+(define-primop + : (→ Nat Nat Nat))
+
+(begin-for-syntax
+  (define (expose t)
+    (cond [(identifier? t)
+           (define sub (typeof t #:tag 'sub))
+           (if sub (expose sub) t)]
+          [else t]))
+  #;(define (type-eval t)
+    (expose (stlc:type-eval t)))
+  #;(current-type-eval type-eval)
+  ;; extend to handle new ∀
+  (define (type=? τ1 τ2)
+    (syntax-parse (list τ1 τ2)
+      [(((~literal #%plain-lambda) (x:id ...) k1 ... t1)
+        ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
+       #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
+       #:when (= (stx-length #'(x ...)) (stx-length #'(k1 ...)))
+       ((current-type=?) (substs #'(k1 ...) #'(x ...) #'t1)
+                         (substs #'(k2 ...) #'(y ...) #'t2))]
+      [_ (or (sysf:type=? τ1 τ2) (stlc:type=? τ1 τ2))]))
+  (current-type=? type=?)
+  (current-typecheck-relation (current-sub?)))
+
+;; TODO: shouldnt really support non-bounded (ie, no <: annotation) ∀, etc
+;; but support for now, so old tests pass
+(define-syntax (∀ stx)
+  (syntax-parse stx #:datum-literals (<:)
+    [(_ ([X:id <: τ] ...) ~! body)
+     ;; CORRECTION: cant subst immediately, need to extend type=? instead
+     ;; subst immediately
+     ;; - need to save τ ... to verify during inst
+     ;; - but otherwise, since the typecheckrelation is sub?,
+     ;;   no behavior is changed by replacing X with τ
+     (syntax/loc stx (#%plain-lambda (X ...) τ ... body))]
+    [(_ x ...) #'(sysf:∀ x ...)]))
+
+(define-syntax (Λ stx)
+  (syntax-parse stx #:datum-literals (<:)
+    [(_ ([tv:id <: τsub] ...) ~! e)
+     ;; NOTE: we are storing the subtyping relation of tv and τsub in the
+     ;; "environment", as we store type annotations
+     ;; So eval-type should be extended to "lookup" the subtype relation.
+     ;; This is analogous to "expose" in TaPL, fig 28-1
+     #:with (_ (tv- ...) (e-) (τ)) (infer #'(e) #:ctx #'([tv : τsub] ...) #:tag 'sub)
+     (⊢ #'e- #'(∀ ([tv- <: τsub] ...) τ))]
+    [(_ x ...) #'(sysf:Λ x ...)]))
+(define-syntax (inst stx)
+  (syntax-parse stx
+    [(_ e τ:type ...)
+     #:with (e- ∀τ) (infer+erase #'e)
+     #:with ((~literal #%plain-lambda) (tv:id ...) τ_sub ... τ_body) #'∀τ
+     #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
+     (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]
+    [(_ e τ:type ...) ; need to ensure no types (ie bounds) in lam (ie expanded ∀) body
+     #:with (e- ∀τ) (infer+erase #'e)
+     #:with ((~literal #%plain-lambda) (tv:id ...) τ_body) #'∀τ
+     #'(sysf:inst e τ ...)]))
+
+;; TODO: refactor to avoid reimplementing app/tc and others below, just to add expose
+(define-syntax (app/tc stx)
+  (syntax-parse stx
+    [(_ e_fn e_arg ...)
+     #:with (e_fn- τ_fn_unexposed) (infer+erase #'e_fn)
+     #:with τ_fn (expose #'τ_fn_unexposed)
+     #:fail-unless (→? #'τ_fn)
+                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+     #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
+     #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+     #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
+                   (string-append
+                    (format
+                     "Wrong number of args given to function ~a:\ngiven: "
+                     (syntax->datum #'e_fn))
+                    (string-join
+                     (map
+                      (λ (e t) (format "~a : ~a" e t))
+                      (syntax->datum #'(e_arg ...))
+                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+                     ", ")
+                    (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
+     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+                   (string-append
+                    (format
+                     "Arguments to function ~a have wrong type:\ngiven: "
+                     (syntax->datum #'e_fn))
+                    (string-join
+                     (map
+                      (λ (e t) (format "~a : ~a" e t))
+                      (syntax->datum #'(e_arg ...))
+                      (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
+                     ", ")
+                    "\nexpected arguments with type: "
+                    (string-join
+                     (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ ...))))
+                     ", "))
+     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+(define-syntax (proj stx)
+  (syntax-parse stx #:literals (quote)
+    [(_ rec l:str ~!)
+     #:with (rec- τ_rec_unexposed) (infer+erase #'rec)
+     #:with τ_rec (expose #'τ_rec_unexposed)
+     #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
+     #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
+     #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
+     (⊢ #'(cadr (assoc l rec)) #'τ_match)]
+    [(_ e ...) #'(stlc:proj e ...)]))
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
index f0db35b..8239d24 100644
--- a/tapl/stlc+reco+var.rkt
+++ b/tapl/stlc+reco+var.rkt
@@ -56,9 +56,9 @@
      #'(stlc:tup e ...)]))
 (define-syntax (proj stx)
   (syntax-parse stx #:literals (quote)
-    [(_ rec l:str)
+    [(_ rec l:str ~!)
      #:with (rec- τ_rec) (infer+erase #'rec)
-     #:fail-unless (×? #'τ_rec) "not record type"
+     #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
      #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
      #:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
      (⊢ #'(cadr (assoc l rec)) #'τ_match)]
diff --git a/tapl/tests/fsub-tests.rkt b/tapl/tests/fsub-tests.rkt
index 19d47ca..083fb6a 100644
--- a/tapl/tests/fsub-tests.rkt
+++ b/tapl/tests/fsub-tests.rkt
@@ -1,6 +1,76 @@
 #lang s-exp "../fsub.rkt"
 (require "rackunit-typechecking.rkt")
 
+;; examples from tapl ch26, bounded quantification
+;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck)
+(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+
+(define ra (tup ["a" = 0]))
+(check-type ((λ ([x : (× [: "a" Int])]) x) ra)
+            : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
+(define rab (tup ["a" = 0]["b" = #t]))
+(check-type ((λ ([x : (× [: "a" Int])]) x) rab)
+            : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+
+(check-type (proj ((λ ([x : (× [: "a" Int])]) x) rab) "a")
+            : Int ⇒ 0)
+
+(check-type (proj ((inst (Λ (X) (λ ([x : X]) x))
+                         (× [: "a" Int][: "b" Bool]))
+                   rab) "b")
+            : Bool ⇒ #t)
+
+(define f2 (λ ([x : (× [: "a" Nat])]) (tup ["orig" = x] ["asucc" = (+ 1 (proj x "a"))])))
+(check-type f2 : (→ (× [: "a" Nat]) (× [: "orig" (× [: "a" Nat])] [: "asucc" Nat])))
+(check-type (f2 ra) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
+(check-type (f2 rab) : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat]))
+
+(define f2poly
+  (Λ ([X <: (× [: "a" Nat])])
+     (λ ([x : X])
+       (tup ["orig" = x]["asucc" = (+ (proj x "a") 1)]))))
+
+(check-type f2poly : (∀ ([X <: (× [: "a" Nat])]) (→ X (× [: "orig" X][: "asucc" Nat]))))
+
+;; inst f2poly with (× [: "a" Nat])
+(check-type (inst f2poly (× [: "a" Nat]))
+            : (→ (× [: "a" Nat])
+                 (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])))
+(check-type ((inst f2poly (× [: "a" Nat])) ra)
+            : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
+            ⇒ (tup ["orig" = ra]["asucc" = 1]))
+
+(check-type ((inst f2poly (× [: "a" Nat])) rab)
+            : (× [: "orig" (× [: "a" Nat])][: "asucc" Nat])
+            ⇒ (tup ["orig" = rab]["asucc" = 1]))
+
+(typecheck-fail (proj (proj ((inst f2poly (× [: "a" Nat])) rab) "orig") "b"))
+
+;; inst f2poly with (× [: "a" Nat][: "b" Bool])
+(check-type (inst f2poly (× [: "a" Nat][: "b" Bool]))
+            : (→ (× [: "a" Nat][: "b" Bool])
+                 (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])))
+(typecheck-fail ((inst f2poly (× [: "a" Nat][: "b" Bool])) ra))
+
+(check-type ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab)
+            : (× [: "orig" (× [: "a" Nat][: "b" Bool])][: "asucc" Nat])
+            ⇒ (tup ["orig" = rab]["asucc" = 1]))
+
+(check-type (proj (proj ((inst f2poly (× [: "a" Nat][: "b" Bool])) rab) "orig") "b")
+            : Bool ⇒ #t)
+
+;; make sure inst still checks args
+(typecheck-fail (inst (Λ ([X <: Nat]) 1) Int))
+
+; ch28
+(define f (Λ ([X <: (→ Nat Nat)]) (λ ([y : X]) (y 5))))
+(check-type f : (∀ ([X <: (→ Nat Nat)]) (→ X Nat)))
+(check-type (inst f (→ Nat Nat)) : (→ (→ Nat Nat) Nat))
+(check-type (inst f (→ Int Nat)) : (→ (→ Int Nat) Nat))
+(check-type ((inst f (→ Int Nat)) (λ ([z : Int]) 5)) : Nat)
+(check-type ((inst f (→ Int Nat)) (λ ([z : Num]) 5)) : Nat)
+(typecheck-fail ((inst f (→ Int Nat)) (λ ([z : Nat]) 5)))
+
 
 ;; old sysf tests -------------------------------------------------------------
 (check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X)))
@@ -51,20 +121,22 @@
 ;;; previous tests -------------------------------------------------------------
 (check-type 1 : Int)
 (check-not-type 1 : (→ Int Int))
-(typecheck-fail "one") ; unsupported literal
-(typecheck-fail #f) ; unsupported literal
+;; strings and boolean literals now ok
+;(typecheck-fail "one") ; unsupported literal
+;(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 (λ ([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)
+;; edited from sysf test to handle subtyping
+(check-type ((λ ([f : (→ Nat Nat Nat)] [x : Nat] [y : Nat]) (f x y)) + 1 2) : Num ⇒ 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)
+(check-type ((λ ([x : Nat]) (+ x x)) 10) : Num ⇒ 20)
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index aefec3b..55afd2d 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -16,6 +16,7 @@
 ;; subtyping
 (require "stlc+sub-tests.rkt")
 (require "stlc+reco+sub-tests.rkt")
+(require "fsub-tests.rkt")
 
 ;; system F
 (require "sysf-tests.rkt")
diff --git a/tapl/tests/stlc+reco+sub-tests.rkt b/tapl/tests/stlc+reco+sub-tests.rkt
index 474ae32..9072fc1 100644
--- a/tapl/tests/stlc+reco+sub-tests.rkt
+++ b/tapl/tests/stlc+reco+sub-tests.rkt
@@ -21,7 +21,21 @@
 (check-type (tup ["plus" = +]) : (× [: "plus" (→ Int Num Top)]))
 (check-type (tup ["plus" = +] ["mul" = *]) : (× [: "plus" (→ Int Num Top)]))
 
-;; previous record tests
+;; examples from tapl ch26, bounded quantification
+(check-type (λ ([x : (× [: "a" Int])]) x) : (→ (× [: "a" Int]) (× [: "a" Int])))
+
+(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]))
+            : (× [: "a" Int]) ⇒ (tup ["a" = 0]))
+(check-type ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t]))
+            : (× [: "a" Int]) ⇒ (tup ["a" = 0]["b" = #t]))
+
+(check-type (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "a")
+            : Int ⇒ 0)
+
+;; this should work! but needs bounded quantification, see fsub.rkt
+(typecheck-fail (proj ((λ ([x : (× [: "a" Int])]) x) (tup ["a" = 0]["b" = #t])) "b"))
+
+;; previous record tests ------------------------------------------------------
 ;; records (ie labeled tuples)
 (check-type "Stephen" : String)
 (check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 6619298..d61b3f4 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -127,12 +127,12 @@
   ;; ⊢ : Syntax Type -> Syntax
   ;; Attaches type τ to (expanded) expression e.
   ;; must eval here, to catch unbound types
-  (define (⊢ e τ)
-    (syntax-property e 'type (syntax-local-introduce ((current-type-eval) τ))))
+  (define (⊢ e τ #:tag [tag 'type])
+    (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ))))
   
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
-  (define (typeof stx) (syntax-property stx 'type))
+  (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
   
   ;; infers type and erases types in a single expression,
   ;; in the context of the given bindings and their types
@@ -161,7 +161,7 @@
   ;; expanded before wrapping in lambda
   ;; - This caused one problem in fomega2.rkt #%app, but I just had to expand
   ;; the types before typechecking, which is acceptable
-  (define (infer es #:ctx [ctx null] #:tvs [tvs null])
+  (define (infer es #:ctx [ctx null] #:tvs [tvs null] #:tag [tag 'type])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
        #:with (e ...) es
@@ -175,7 +175,7 @@
        (expand/df
         #`(λ #,tvs
             (λ (x ...)
-              (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
+              (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ #:tag '#,tag))] ...)
                 (#%expression e) ...))))
        (list #'tvs+ #'xs+ #'(e+ ...)
              (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
@@ -184,7 +184,8 @@
   (define current-typecheck-relation (make-parameter #f))
   (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
   (define (typechecks? τs1 τs2)
-    (stx-andmap (current-typecheck-relation) τs1 τs2))
+    (and (= (stx-length τs1) (stx-length τs2))
+         (stx-andmap (current-typecheck-relation) τs1 τs2)))
   
   (define current-type-eval (make-parameter #f))