diff --git a/turnstile/examples/dep2.rkt b/turnstile/examples/dep2.rkt
index 743f394..95c3dca 100644
--- a/turnstile/examples/dep2.rkt
+++ b/turnstile/examples/dep2.rkt
@@ -7,7 +7,8 @@
 
 (provide (rename-out [#%type *])
          Π → ∀
-;;       = eq-refl eq-elim
+       = eq-refl
+       ;;eq-elim
 ;;          Nat Z S nat-ind
          λ
          #%app ann
@@ -37,6 +38,8 @@
   (define old-relation (current-typecheck-relation))
   (current-typecheck-relation
    (lambda (t1 t2)
+     ;; (pretty-print (stx->datum t1))
+     ;; (pretty-print (stx->datum t2))
      ;; assumed #f can only come from (typeof #%type)
      ;; (so this wont work when interacting with untyped code)
      (or (and (false? (syntax-e t1)) (#%type? t2)) ; set Type : Type
@@ -53,7 +56,7 @@
   ;; TODO: check that τ_in and τ_out have #%type?
   [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _] [τ_in ≫ τ_in- ⇒ _] ...]
   -------
-  [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #,Type #;#%type])
+  [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #%type])
 
 ;; abbrevs for Π
 (define-simple-macro (→ τ_in ... τ_out)
@@ -72,20 +75,20 @@
        [(_ ([x:id : τ_in] ...)  τ_out)
         #'(~∀ (x ...) (~→ τ_in ... τ_out))]))))
 
-;; ;; equality -------------------------------------------------------------------
-;; (define-internal-type-constructor =)
-;; (define-typed-syntax (= t1 t2) ≫
-;;   [⊢ t1 ≫ t1- ⇒ _] [⊢ t2 ≫ t2- ⇒ _]
-;;   ;; #:do [(printf "t1: ~a\n" (stx->datum #'t1-))
-;;   ;;       (printf "t2: ~a\n" (stx->datum #'t2-))]
-;; ;  [t1- τ= t2-]
-;;   ---------------------
-;;   [⊢ (=- t1- t2-) ⇒ #,(expand/df #'#%type)])
+;; equality -------------------------------------------------------------------
+(define-internal-type-constructor =)
+(define-typed-syntax (= t1 t2) ≫
+  [⊢ t1 ≫ t1- ⇒ _] [⊢ t2 ≫ t2- ⇒ _]
+  ;; #:do [(printf "t1: ~a\n" (stx->datum #'t1-))
+  ;;       (printf "t2: ~a\n" (stx->datum #'t2-))]
+;  [t1- τ= t2-]
+  ---------------------
+  [⊢ (=- t1- t2-) ⇒ #%type])
 
-;; (define-typed-syntax (eq-refl e) ≫
-;;   [⊢ e ≫ e- ⇒ _]
-;;   ----------
-;;   [⊢ (#%app- void-) ⇒ (= e- e-)])
+(define-typed-syntax (eq-refl e) ≫
+  [⊢ e ≫ e- ⇒ _]
+  ----------
+  [⊢ (#%app- void-) ⇒ (= e- e-)])
 
 ;; (define-typed-syntax (eq-elim t P pt w peq) ≫
 ;;   [⊢ t ≫ t- ⇒ ty]
@@ -145,15 +148,29 @@
 ;;       [(~literal +-) (stx+ args)]
 ;;       [(~literal zero?-) (apply zero? (stx->nats args))])))
 
+;; TODO: fix orig after subst
+(define-syntax app/eval
+  (syntax-parser
+    ;; TODO: apply to only lambda args or all args?
+    [(_ (~and f ((~literal #%plain-lambda) (x ...) e)) e_arg ...)
+     ;; TODO: need to replace all #%app- in this result with app/eval again
+     ;; and then re-expand
+     (substs #'(e_arg ...) #'(x ...) #'e)]
+    [(_ f . args)
+     #'(#%app- f . args)]))
+     
+;; TODO: fix orig after subst
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫
+;   #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))]
 ;   [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)]
    [⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)]
+;   #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn-))]
    #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
                  (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
    [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... ; typechecking args
    -----------------------------
-   [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out]])
+   [⊢ (app/eval e_fn- e_arg- ...) ⇒ #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]])
    
 #;(define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫ ; apply lambda
@@ -299,6 +316,7 @@
 ;;   [⊢ (#%app- void-) ⇒ ty])
 
 ;; top-level ------------------------------------------------------------------
+;; TODO: shouldnt need define-type-alias, should be same as define
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ);τ:any-type)
diff --git a/turnstile/examples/tests/dep2-tests.rkt b/turnstile/examples/tests/dep2-tests.rkt
index e3dc4bd..457b546 100644
--- a/turnstile/examples/tests/dep2-tests.rkt
+++ b/turnstile/examples/tests/dep2-tests.rkt
@@ -116,7 +116,9 @@
 ;; booleans -------------------------------------------------------------------
 
 ;; Bool base type
+;; TODO: use define instead of define-type-alias
 (define-type-alias Bool (∀ (A) (→ A A A)))
+(check-type Bool : *)
 
 ;; Bool terms
 (define T (λ ([A : *]) (λ ([x : A][y : A]) x)))
@@ -124,98 +126,120 @@
 (check-type T : Bool)
 (check-type F : Bool)
 ;; check infer case
-(define T2 (λ ([bool : *]) (λ ([x : bool][y : bool]) x)))
-(define F2 (λ ([bool : *]) (λ ([x : bool][y : bool]) y)))
+(define T2 (λ ([abool : *]) (λ ([x : abool][y : abool]) x)))
+(define F2 (λ ([abool : *]) (λ ([x : abool][y : abool]) y)))
 (check-type T2 : Bool)
 (check-type F2 : Bool)
-(define T3 : Bool (λ (bool) (λ (x y) x)))
-(define F3 : Bool (λ (bool) (λ (x y) y)))
+(define T3 : Bool (λ (abool) (λ (x y) x)))
+(define F3 : Bool (λ (abool) (λ (x y) y)))
 (check-type T3 : Bool)
 (check-type F3 : Bool)
 
 ;; defining `and` requires instantiating polymorphic types
-; (define and (λ ([x : Bool][y : Bool]) ((x Bool) y F)))
-;(check-type and : (→ Bool Bool Bool))
+(define and (λ ([x : Bool][y : Bool]) ((x Bool) y F)))
+(check-type and : (→ Bool Bool Bool))
+(define or (λ ([x : Bool][y : Bool]) ((x Bool) T y)))
+(check-type or : (→ Bool Bool Bool))
+(define not (λ ([x : Bool]) ((x Bool) F T)))
+(check-type not : (→ Bool Bool))
 
-;; ;; And type constructor, ie type-level fn
-;; (define-type-alias And
-;;   (λ ([A : *][B : *])
-;;     (∀ (C) (→ (→ A B C) C))))
-;; (check-type And : (→ * * *))
+;; `And` type constructor, ie type-level fn
+(define-type-alias And
+  (λ ([P : *][Q : *])
+    (∀ (C) (→ (→ P Q C) C))))
+(check-type And : (→ * * *))
 
-;; ;; And type intro
-;; (define ∧
-;;   (λ ([A : *][B : *])
-;;     (λ ([x : A][y : B])
-;;       (λ ([C : *])
-;;         (λ ([f : (→ A B C)])
-;;           (f x y))))))
-;; (check-type ∧ : (∀ (A B) (→ A B (And A B))))
+;; And type intro (logical conj)
+(define ∧
+  (λ ([P : *][Q : *])
+    (λ ([p : P][q : Q])
+      (λ ([C : *])
+        (λ ([f : (→ P Q C)])
+          (f p q))))))
+(check-type ∧ : (∀ (P Q) (→ P Q (And P Q))))
 
-;; ;; And type elim
-;; (define proj1
-;;   (λ ([A : *][B : *])
-;;     (λ ([e∧ : (And A B)])
-;;       ((e∧ A) (λ ([x : A][y : B]) x)))))
-;; (define proj2
-;;   (λ ([A : *][B : *])
-;;     (λ ([e∧ : (And A B)])
-;;       ((e∧ B) (λ ([x : A][y : B]) y)))))
-;; ;; bad proj2: (e∧ A) should be (e∧ B)
-;; (typecheck-fail
-;;  (λ ([A : *][B : *])
-;;    (λ ([e∧ : (And A B)])
-;;      ((e∧ A) (λ ([x : A][y : B]) y))))
-;;  #:verb-msg
-;;  "expected (→ A B C), given (Π ((x : A) (y : B)) B)")
-;; (check-type proj1 : (∀ (A B) (→ (And A B) A)))
-;; (check-type proj2 : (∀ (A B) (→ (And A B) B)))
+;; `And` type elim
+(define proj1
+  (λ ([P : *][Q : *])
+    (λ ([e : (And P Q)])
+      ((e P) (λ ([x : P][y : Q]) x)))))
+(define proj2
+  (λ ([P : *][Q : *])
+    (λ ([e : (And P Q)])
+      ((e Q) (λ ([x : P][y : Q]) y)))))
+;; bad proj2: (e A) should be (e B)
+(typecheck-fail
+ (λ ([P : *][Q : *])
+   (λ ([e : (And P Q)])
+     ((e P) (λ ([x : P][y : Q]) y))))
+ #:verb-msg
+ "expected (→ P Q C), given (Π ((x : P) (y : Q)) Q)")
+(check-type proj1 : (∀ (P Q) (→ (And P Q) P)))
+(check-type proj2 : (∀ (P Q) (→ (And P Q) Q)))
 
-;; ;((((conj q) p) (((proj2 p) q) a)) (((proj1 p) q) a)))))
-;; (define and-commutes
-;;   (λ ([A : *][B : *])
-;;     (λ ([e∧ : (And A B)])
-;;       ((∧ B A) ((proj2 A B) e∧) ((proj1 A B) e∧)))))
-;; ;; bad and-commutes, dont flip A and B: (→ (And A B) (And A B))
-;; (typecheck-fail
-;;  (λ ([A : *][B : *])
-;;    (λ ([e∧ : (And A B)])
-;;      ((∧ A B) ((proj2 A B) e∧) ((proj1 A B) e∧))))
-;;  #:verb-msg
-;;  "#%app: type mismatch: expected A, given C") ; TODO: err msg should be B not C?
-;; (check-type and-commutes : (∀ (A B) (→ (And A B) (And B A))))
+;; proj1, no annotations
+(check-type (λ (P Q) (λ (e) ((e P) (λ (x y) x))))
+            : (∀ (P Q) (→ (And P Q) P)))
+;; proj2, no annotations
+(check-type (λ (P Q) (λ (e) ((e Q) (λ (x y) y))))
+            : (∀ (P Q) (→ (And P Q) Q)))
+(typecheck-fail (ann (λ (P Q) (λ (e) ((e Q) (λ (x y) x))))
+                     : (∀ (P Q) (→ (And P Q) Q)))
+ #:with-msg "expected C, given P") ; TODO: err msg, fix orig
+(typecheck-fail (ann (λ (P Q) (λ (e) ((e P) (λ (x y) y))))
+                     : (∀ (P Q) (→ (And P Q) Q)))
+ #:with-msg "expected C, given Q") ; TODO: err msg
 
-;; ;; nats -----------------------------------------------------------------------
-;; (define-type-alias nat (∀ (A) (→ A (→ A A) A)))
+;((((conj q) p) (((proj2 p) q) a)) (((proj1 p) q) a)))))
+(define and-commutes
+  (λ ([A : *][B : *])
+    (λ ([e : (And A B)])
+      ((∧ B A) ((proj2 A B) e) ((proj1 A B) e)))))
+;; bad and-commutes, dont flip A and B: (→ (And A B) (And A B))
+(typecheck-fail
+ (λ ([A : *][B : *])
+   (λ ([e : (And A B)])
+     ((∧ A B) ((proj2 A B) e) ((proj1 A B) e))))
+ #:verb-msg
+ "#%app: type mismatch: expected P, given C") ; TODO: err msg
+(check-type and-commutes : (∀ (A B) (→ (And A B) (And B A))))
 
-;; (define-type-alias z (λ ([Ty : *]) (λ ([zero : Ty][succ : (→ Ty Ty)]) zero)))
-;; (define-type-alias s (λ ([n : nat])
-;;                        (λ ([Ty : *])
-;;                          (λ ([zero : Ty][succ : (→ Ty Ty)])
-;;                            (succ ((n Ty) zero succ))))))
-;; (check-type z : nat)
-;; (check-type s : (→ nat nat))
+;; nats -----------------------------------------------------------------------
+(define-type-alias nat (∀ (A) (→ A (→ A A) A)))
+(check-type nat : *)
 
-;; (define-type-alias one (s z))
-;; (define-type-alias two (s (s z)))
-;; (check-type one : nat)
-;; (check-type two : nat)
+(define-type-alias z (λ ([Ty : *]) (λ ([zero : Ty][succ : (→ Ty Ty)]) zero)))
+(define-type-alias s (λ ([n : nat])
+                       (λ ([Ty : *])
+                         (λ ([zero : Ty][succ : (→ Ty Ty)])
+                           (succ ((n Ty) zero succ))))))
+(check-type z : nat)
+(check-type s : (→ nat nat))
 
-;; (define-type-alias plus
-;;   (λ ([x : nat][y : nat])
-;;     ((x nat) y s)))
-;; (check-type plus : (→ nat nat nat))
+(define-type-alias one (s z))
+(define-type-alias two (s (s z)))
+(check-type one : nat)
+(check-type two : nat)
 
-;; ;; equality -------------------------------------------------------------------
+(define-type-alias plus
+  (λ ([x : nat][y : nat])
+    ((x nat) y s)))
+(check-type plus : (→ nat nat nat))
+(check-type (λ (x y) ((x nat) y s)) : (→ nat nat nat))
 
-;; (check-type (eq-refl one) : (= one one))
-;; (check-type (eq-refl one) : (= (s z) one))
-;; (check-type (eq-refl two) : (= (s (s z)) two))
-;; (check-type (eq-refl two) : (= (s one) two))
-;; (check-type (eq-refl two) : (= two (s one)))
-;; (check-type (eq-refl two) : (= (s (s z)) (s one)))
-;; (check-type (eq-refl two) : (= (plus one one) two))
-;; (check-not-type (eq-refl two) : (= (plus one one) one))
+;; equality -------------------------------------------------------------------
+
+(check-type (eq-refl one) : (= one one))
+(typecheck-fail (ann (eq-refl one) : (= two one))
+ #:verb-msg "expected (= two one), given (= one one)")
+(check-type (eq-refl one) : (= (s z) one))
+(check-type (eq-refl two) : (= (s (s z)) two))
+(check-type (eq-refl two) : (= (s one) two))
+(check-type (eq-refl two) : (= two (s one)))
+(check-type (eq-refl two) : (= (s (s z)) (s one)))
+;; the following example requires recursive expansion after eval/app
+;(check-type (eq-refl two) : (= (plus one one) two))
+;(check-not-type (eq-refl two) : (= (plus one one) one))
 
 ;; ;; symmetry of =
 ;; (check-type