diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt
index 42f97ca..b7d373a 100644
--- a/macrotypes/stx-utils.rkt
+++ b/macrotypes/stx-utils.rkt
@@ -7,6 +7,7 @@
 (define id? identifier?)
 (define free-id=? free-identifier=?)
 (define fmt format)
+(define stx-e syntax-e)
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 (define (stx-caddr stx) (stx-cadr (stx-cdr stx)))
diff --git a/turnstile/examples/dep.rkt b/turnstile/examples/dep.rkt
index a15930a..0a5faf2 100644
--- a/turnstile/examples/dep.rkt
+++ b/turnstile/examples/dep.rkt
@@ -1,8 +1,12 @@
 #lang turnstile/lang
 
-; Π  λ ≻ ⊢ ≫ ⇒ ∧ (bidir ⇒ ⇐)
+; Π  λ ≻ ⊢ ≫ → ∧ (bidir ⇒ ⇐)
 
-(provide (rename-out [#%type *]) Π → ∀ λ #%app ann define define-type-alias)
+(provide (rename-out [#%type *])
+         Π → ∀ = eq-refl eq-elim
+         Nat Z S nat-ind
+         λ #%app ann
+         define define-type-alias)
 
 #;(begin-for-syntax
   (define old-ty= (current-type=?))
@@ -14,6 +18,7 @@
   (current-typecheck-relation (current-type=?)))
 
 ;(define-syntax-category : kind)
+(define-base-type Nat)
 (define-internal-type-constructor →)
 (define-internal-binding-type ∀)
 ;; TODO: how to do Type : Type
@@ -37,6 +42,36 @@
        [(_ ([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)])
+
+(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]
+; [⊢ P ≫ P- ⇒ _] 
+; [⊢ pt ≫ pt- ⇒ _]
+; [⊢ w ≫ w- ⇒ _]
+; [⊢ peq ≫ peq- ⇒ _]
+  [⊢ P ≫ P- ⇐ (→ ty #%type)]
+  [⊢ pt ≫ pt- ⇐ (P- t-)]
+  [⊢ w ≫ w- ⇐ ty]
+  [⊢ peq ≫ peq- ⇐ (= t- w-)]
+  --------------
+  [⊢ (#%app- void-) ⇒ (P- w-)])
+
+;; lambda and #%app -----------------------------------------------------------
+
 ;; TODO: add case with expected type + annotations
 ;; - check that annotations match expected types
 (define-typed-syntax λ
@@ -49,30 +84,165 @@
    ---------
    [⊢ (λ- (x- ...) e-)]])
 
-;; TODO: do beta on terms?
+;; classes for matching number literals
+(begin-for-syntax
+  (define-syntax-class nat
+    (pattern (~or n:exact-nonnegative-integer (_ n:exact-nonnegative-integer))
+             #:attr val
+             #'n))
+  (define-syntax-class nats
+    (pattern (n:nat ...) #:attr vals #'(n.val ...)))
+  ; extract list of quoted numbers
+  (define stx->nat (syntax-parser [n:nat (stx-e #'n.val)]))
+  (define (stx->nats stx) (stx-map stx->nat stx))
+  (define (stx+ ns) (apply + (stx->nats ns)))
+  (define (delta op-stx args)
+    (syntax-parse op-stx
+      [(~literal +-) (stx+ args)]
+      [(~literal zero?-) (apply zero? (stx->nats args))])))
+
 (define-typed-syntax #%app
   [(_ e_fn e_arg ...) ≫ ; apply lambda
-   [⊢ e_fn ≫ (_ (x ...) e ~!) ⇒ (~Π ([X : τ_in] ...) τ_out)]
-   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
-                 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
-   [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+   #:do[(printf "applying (1) ~a\n" (stx->datum #'e_fn))]
+   [⊢ e_fn ≫ (~and e_fn- (_ (x:id ...) e ~!)) ⇒ (~Π ([X : τ_inX] ...) τ_outX)]
+   #:do[(printf "e_fn-: ~a\n" (stx->datum #'e_fn-))
+        (printf "args: ~a\n" (stx->datum #'(e_arg ...)))]
+   #:fail-unless (stx-length=? #'[τ_inX ...] #'[e_arg ...])
+                 (num-args-fail-msg #'e_fn #'[τ_inX ...] #'[e_arg ...])
+   [⊢ e_arg ≫ e_arg- ⇒ ty-argX] ... ; typechecking args must be fold; do in 2 steps
+   #:do[(define (ev e)
+          (syntax-parse e
+;            [_ #:do[(printf "eval: ~a\n" (stx->datum e))] #:when #f #'(void)]
+            [(~or _:id
+;                  ((~literal #%plain-lambda) . _)
+                  (~= _ _)
+                  ~Nat
+                  ((~literal quote) _))
+             e]
+            ;; handle nums
+            [((~literal #%plain-app)
+              (~and op (~or (~literal +-) (~literal zero?-)))
+              . args:nats)
+             #`#,(delta #'op #'args.vals)]
+            [((~literal #%plain-app) (~and f ((~literal #%plain-lambda) . b)) . rst)
+             (expand/df #`(#%app f . #,(stx-map ev #'rst)))]
+            [(x ...)
+             ;; #:do[(printf "t before: ~a\n" (typeof e))
+             ;;      (printf "t after: ~a\n" (typeof #`#,(stx-map ev #'(x ...))))]
+             (syntax-property #`#,(stx-map ev #'(x ...)) ': (typeof e))]
+            [_  e] ; other literals
+            #;[es (stx-map L #'es)]))]
+   #:with (τ_in ... τ_out)
+          (stx-map
+           (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t)))
+           #'(τ_inX ... τ_outX))
+   #:with (ty-arg ...)
+          (stx-map
+           (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t)))
+           #'(ty-argX ...))
+;   #:do[(printf "vars: ~a\n" #'(X ...))]
+;   #:when (stx-andmap (λ (t1 t2)(displayln (stx->datum t1)) (displayln (stx->datum t2)) (displayln (typecheck? t1 t2)) #;(typecheck? t1 t2)) #'(ty-arg ...) #'(τ_in ...))
+   ;; #:do[(stx-map
+   ;;       (λ (tx t) (printf "ty_in inst: \n~a\n~a\n" (stx->datum tx) (stx->datum t)))
+   ;;       #'(τ_inX ...)          #'(τ_in ...))]
+   [⊢ e_arg ≫ _ ⇐ τ_in] ...
+  ;; #:do[(printf "res e =\n~a\n" (stx->datum (substs #'(e_arg- ...) #'(x ...) #'e)))
+  ;;      (printf "res t = ~a\n" (stx->datum (substs #'(e_arg- ...) #'(X ...) #'τ_out)))]
+   #:with res-e (let L ([e (substs #'(e_arg- ...) #'(x ...) #'e)]) ; eval
+                  (syntax-parse e
+                    [(~or _:id
+                          ((~literal #%plain-lambda) . _)
+                          (~Π ([_ : _] ...) _)
+                          (~= _ _)
+                          ~Nat)
+                     e]
+                    ;; handle nums
+                    [((~literal #%plain-app)
+                      (~and op (~or (~literal +-) (~literal zero?-)))
+                      . args:nats)
+                     #`#,(delta #'op #'args.vals)]
+                    [((~literal #%plain-app) . rst)
+                     (expand/df #`(#%app . #,(stx-map L #'rst)))]
+                    [_ e] ; other literals
+                    #;[es (stx-map L #'es)]))
+   ;; #:with res-ty (syntax-parse (substs #'(e_arg- ...) #'(X ...) #'τ_out)
+   ;;                 [((~literal #%plain-app) . rst) (expand/df #'(#%app . rst))]
+   ;;                 [other-ty #'other-ty])
    --------
-   [⊢ #,(substs #'(e_arg- ...) #'(x ...) #'e) ⇒
-      #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]]
+   [⊢ res-e #;#,(substs #'(e_arg- ...) #'(x ...) #'e) ⇒ τ_out
+            #;#,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]]
   [(_ e_fn e_arg ... ~!) ≫ ; apply var
-   [⊢ e_fn ≫ e_fn- ⇒ (~Π ([X : τ_in] ...) τ_out)]
-   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
-                 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
-   [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+;   #:do[(printf "applying (2) ~a\n" (stx->datum #'e_fn))]
+   [⊢ e_fn ≫ e_fn- ⇒ ty-fn]
+;   #:do[(printf "e_fn- ty: ~a\n" (stx->datum #'ty-fn))]
+   [⊢ e_fn ≫ _ ⇒ (~Π ([X : τ_inX] ...) τ_outX)]
+;   #:do[(printf "e_fn- no: ~a\n" (stx->datum #'e_fn-))
+;        (printf "args: ~a\n" (stx->datum #'(e_arg ...)))]
+   ;; #:with e_fn- (syntax-parse #'e_fn*
+   ;;                [((~literal #%plain-app) . rst) (expand/df #'(#%app . rst))]
+   ;;                [other #'other])
+   #:fail-unless (stx-length=? #'[τ_inX ...] #'[e_arg ...])
+                 (num-args-fail-msg #'e_fn #'[τ_inX ...] #'[e_arg ...])
+   [⊢ e_arg ≫ e_arg- ⇒ ty-argX] ... ; typechecking args must be fold; do in 2 steps
+   #:do[(define (ev e)
+          (syntax-parse e
+;            [_ #:do[(printf "eval: ~a\n" (stx->datum e))] #:when #f #'(void)]
+            [(~or _:id
+;                  ((~literal #%plain-lambda) . _)
+                  (~= _ _)
+                  ~Nat
+                  ((~literal quote) _))
+             e]
+            ;; handle nums
+            [((~literal #%plain-app)
+              (~and op (~or (~literal +-) (~literal zero?-)))
+              . args:nats)
+             #`#,(delta #'op #'args.vals)]
+            [((~literal #%plain-app) (~and f ((~literal #%plain-lambda) . b)) . rst)
+             (expand/df #`(#%app f . #,(stx-map ev #'rst)))]
+            [(x ...)
+             ;; #:do[(printf "t before: ~a\n" (typeof e))
+             ;;      (printf "t after: ~a\n" (typeof #`#,(stx-map ev #'(x ...))))]
+             (syntax-property #`#,(stx-map ev #'(x ...)) ': (typeof e))]
+            [_  e] ; other literals
+            #;[es (stx-map L #'es)]))]
+   #:with (τ_in ... τ_out)
+          (stx-map
+           (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t)))
+           #'(τ_inX ... τ_outX))
+   #:with (ty-arg ...)
+          (stx-map
+           (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t)))
+           #'(ty-argX ...))
+   ;; #:do[(printf "vars: ~a\n" #'(X ...))]
+   #:when (stx-andmap (λ (e t1 t2)(displayln (stx->datum e))(displayln (stx->datum t1)) (displayln (stx->datum t2)) (displayln (typecheck? t1 t2)) #;(typecheck? t1 t2)) #'(e_arg ...)#'(ty-arg ...) #'(τ_in ...))
+   ;; #:do[(stx-map
+   ;;       (λ (tx t) (printf "ty_in inst: \n~a\n~a\n" (stx->datum tx) (stx->datum t)))
+   ;;       #'(τ_inX ...)          #'(τ_in ...))]
+   [⊢ e_arg ≫ _ ⇐ τ_in] ...
+;  #:do[(printf "res e2 =\n~a\n" (stx->datum #'(#%app- e_fn- e_arg- ...)))
+;       (printf "res t2 = ~a\n" (stx->datum (substs #'(e_arg- ...) #'(X ...) #'τ_out)))]
+   ;; #:with res-e (syntax-parse #'e_fn-
+   ;;                [((~literal #%plain-lambda) . _) (expand/df #'(#%app e_fn- e_arg- ...))]
+   ;;                [other #'(#%app- e_fn- e_arg- ...)])
    --------
-   [⊢ (#%app- e_fn- e_arg- ...) ⇒
-      #,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]])
+   [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out
+      #;#,(expand/df (substs #'(e_arg- ...) #'(X ...) #'τ_out))]])
 
 (define-typed-syntax (ann e (~datum :) τ) ≫
   [⊢ e ≫ e- ⇐ τ]
   --------
   [⊢ e- ⇒ τ])
 
+(define-typed-syntax (if e1 e2 e3) ≫
+  [⊢ e1 ≫ e1- ⇒ _]
+  [⊢ e2 ≫ e2- ⇒ ty]
+  [⊢ e3 ≫ e3- ⇒ _]
+  #:do[(displayln #'(e1 e2 e3))]
+  --------------
+  [⊢ (#%app- void-) ⇒ ty])
+
+;; top-level ------------------------------------------------------------------
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ);τ:any-type)
@@ -111,3 +281,52 @@
         (define- f-
           (stlc+lit:λ ([x : ty] ...)
             (stlc+lit:ann (begin e ...) : ty_out))))]])
+
+
+;; peano nums -----------------------------------------------------------------
+(define-typed-syntax Z
+  [_:id ≫ --- [⊢ 0 ⇒ Nat]])
+
+(define-typed-syntax (S n) ≫
+  [⊢ n ≫ n- ⇐ Nat]
+  -----------
+  [⊢ (#%app- +- n- 1) ⇒ Nat])
+#;(define-typed-syntax (sub1 n) ≫
+  [⊢ n ≫ n- ⇐ Nat]
+  #:do[(displayln #'n-)]
+  -----------
+  [⊢ (#%app- -- n- 1) ⇒ Nat])
+
+;; generalized recursor over natural nums
+;; (cases dispatched in #%app)
+(define- (nat-ind- P z s n) (#%app- void))
+(define-syntax nat-ind
+  (make-variable-like-transformer
+   (assign-type 
+    #'nat-ind-
+    #'(Π ([P : (→ Nat #%type)]
+          [z : (P Z)]
+          [s : (Π ([k : Nat]) (→ (P k) (P (S k))))]
+          [n : Nat])
+         (P n)))))
+
+#;(define-type-alias nat-ind
+  (λ ([P : (→ Nat #%type)]
+      [z : (P Z)]
+      [s : (Π ([k : Nat]) (→ (P k) (P (S k))))]
+      [n : Nat])
+    #'(#%app- nat-ind- P z s n)))
+#;(define-typed-syntax (nat-ind P z s n) ≫
+  [⊢ P ≫ P- ⇐ (→ Nat #%type)]
+;  [⊢ b ≫ b- ⇒ _] ; zero 
+;  [⊢ c ≫ c- ⇒ _] ; succ
+;  [⊢ d ≫ d- ⇒ _]
+  [⊢ z ≫ z- ⇐ (P- Z)] ; zero 
+  [⊢ s ≫ s- ⇐ (Π ([k : Nat]) (→ (P- k) (P- (S k))))] ; succ
+  [⊢ n ≫ n- ⇐ Nat]
+  #:with res (if (typecheck? #'n- (expand/df #'Z))
+                 #'z-
+                 #'(s- (nat-ind P- z- s- (sub1 n-))))
+  ----------------
+  [⊢ res ⇒ (P- n-)])
+;  [≻ (P- d-)])
diff --git a/turnstile/examples/tests/dep-peano.rkt b/turnstile/examples/tests/dep-peano.rkt
new file mode 100644
index 0000000..d0d171a
--- /dev/null
+++ b/turnstile/examples/tests/dep-peano.rkt
@@ -0,0 +1,52 @@
+#lang s-exp "../dep.rkt"
+(require "rackunit-typechecking.rkt")
+
+; Π → λ ∀ ≻ ⊢ ≫ ⇒
+
+;; examples from Prabhakar's Proust paper
+
+;; Peano nums -----------------------------------------------------------------
+
+(define-type-alias nat-rec
+  (λ ([C : *])
+    (λ ([zc : C][sc : (→ C C)])
+      (λ ([n : Nat])
+        (nat-ind (λ ([x : Nat]) C)
+                 zc
+                 (λ ([x : Nat]) sc)
+                 n)))))
+;(check-type nat-rec : (∀ (C) (→ C (→ C C) (→ Nat C))))
+
+(define-type-alias plus
+  (λ ([n : Nat])
+    (((nat-rec (→ Nat Nat))
+      (λ ([m : Nat]) m)
+      (λ ([pm : (→ Nat Nat)])
+        (λ ([x : Nat])
+          (S (pm x)))))
+     n)))
+
+(check-type plus : (→ Nat (→ Nat Nat)))
+
+;(check-type ((plus Z) Z) : Nat -> 0)
+;(check-type ((plus (S Z)) (S Z)) : Nat -> 2)
+;(check-type ((plus (S Z)) Z) : Nat -> 1)
+
+;; ;; plus zero left
+;; (check-type
+;;  (λ ([n : Nat]) (eq-refl n))
+;;  : (Π ([n : Nat]) (= ((plus Z) n) n)))
+
+;; (check-type
+;;  (λ ([n : Nat])
+;;    (nat-ind (λ ([m : Nat]) (= ((plus m) Z) m))
+;;             (eq-refl Z)
+;;             (λ ([k : Nat])
+;;               (λ ([p : (= ((plus k) Z) k)])
+;;                 (eq-elim ((plus k) Z)
+;;                          (λ ([W : Nat]) (= (S ((plus k) Z)) (S W)))
+;;                          (eq-refl (S ((plus k) Z)))
+;;                          k
+;;                          p)))
+;;             n))
+;;  : (Π ([n : Nat]) (= ((plus n) Z) n)))
diff --git a/turnstile/examples/tests/dep-tests.rkt b/turnstile/examples/tests/dep-tests.rkt
index ddb29d2..87d323e 100644
--- a/turnstile/examples/tests/dep-tests.rkt
+++ b/turnstile/examples/tests/dep-tests.rkt
@@ -94,3 +94,54 @@
  #: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))))
+
+;; nats -----------------------------------------------------------------------
+(define-type-alias nat (∀ (A) (→ A (→ A A) 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))
+
+(define-type-alias one (s z))
+(define-type-alias two (s (s z)))
+(check-type one : nat)
+(check-type two : nat)
+
+(define-type-alias plus
+  (λ ([x : nat][y : nat])
+    ((x nat) y s)))
+(check-type plus : (→ nat nat nat))
+
+;; equality -------------------------------------------------------------------
+
+(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))
+
+;; symmetry of =
+(check-type 
+ (λ ([A : *][B : *])
+   (λ ([e : (= A B)])
+     (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e)))
+ : (∀ (A B) (→ (= A B) (= B A))))
+(check-not-type
+ (λ ([A : *][B : *])
+   (λ ([e : (= A B)])
+     (eq-elim A (λ ([W : *]) (= W A)) (eq-refl A) B e)))
+ : (∀ (A B) (→ (= A B) (= A B))))
+
+;; transitivity of =
+(check-type
+ (λ ([X : *][Y : *][Z : *])
+   (λ ([e1 : (= X Y)][e2 : (= Y Z)])
+     (eq-elim Y (λ ([W : *]) (= X W)) e1 Z e2)))
+ : (∀ (A B C) (→ (= A B) (= B C) (= A C))))
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index c6e1212..d9e810a 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -466,6 +466,7 @@
         rule ...+)
      #'(define-syntax (rulename stx)
          (parameterize ([current-check-relation (current-typecheck-relation)]
+                        [current=? (current-type=?)]
                         [current-ev (current-type-eval)]
                         [current-tag (type-key1)])
            (syntax-parse/typecheck stx kw-stuff ... rule ...)))]))