diff --git a/turnstile/examples/dep.rkt b/turnstile/examples/dep.rkt
deleted file mode 100644
index 481e510..0000000
--- a/turnstile/examples/dep.rkt
+++ /dev/null
@@ -1,334 +0,0 @@
-#lang turnstile/lang
-
-; Π  λ ≻ ⊢ ≫ → ∧ (bidir ⇒ ⇐)
-
-(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=?))
-  (current-type=?
-   (λ (t1 t2)
-     (displayln (stx->datum t1))
-     (displayln (stx->datum t2))
-     (old-ty= t1 t2)))
-  (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
-(define-typed-syntax (Π ([X:id : τ_in] ...) τ_out) ≫
-  [[X ≫ X- : τ_in] ... ⊢ [τ_out ≫ τ_out- ⇒ _][τ_in ≫ τ_in- ⇒ _] ...]
-  -------
-  [⊢ (∀- (X- ...) (→- τ_in- ... τ_out-)) ⇒ #,(expand/df #'#%type)])
-;; abbrevs for Π
-(define-simple-macro (→ τ_in ... τ_out)
-  #:with (X ...) (generate-temporaries #'(τ_in ...))
-  (Π ([X : τ_in] ...) τ_out))
-(define-simple-macro (∀ (X ...)  τ)
-  (Π ([X : #%type] ...) τ))
-;; ~Π pattern expander
-(begin-for-syntax
-  (define-syntax ~Π
-    (pattern-expander
-     (syntax-parser
-       [(_ ([x:id : τ_in] ... (~and (~literal ...) ooo)) τ_out)
-        #'(~∀ (x ... ooo) (~→ τ_in ... ooo τ_out))]
-       [(_ ([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 λ
-  [(_ ([x:id : τ_in] ...) e) ≫
-   [[x ≫ x- : τ_in] ... ⊢ [e ≫ e- ⇒ τ_out][τ_in ≫ τ_in- ⇒ _] ...]
-   -------
-   [⊢ (λ- (x- ...) e-) ⇒ (Π ([x- : τ_in-] ...) τ_out)]]
-  [(_ (y:id ...) e) ⇐ (~Π ([x:id : τ_in] ...) τ_out) ≫
-   [[x ≫ x- : τ_in] ... ⊢ #,(substs #'(x ...) #'(y ...) #'e) ≫ e- ⇐ τ_out]
-   ---------
-   [⊢ (λ- (x- ...) e-)]])
-
-;; 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
-;   #: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_argX- ⇒ 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 (ty-arg ...)
-          (stx-map
-           (λ (t) (ev (substs #'(e_argX- ...) #'(X ...) t)))
-           #'(ty-argX ...))
-   #:with (e_arg- ...) (stx-map (λ (e t) (assign-type e t)) #'(e_argX- ...) #'(ty-arg ...))
-   #:with (τ_in ... τ_out)
-          (stx-map
-           (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t)))
-           #'(τ_inX ... τ_outX))
-;   #: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])
-   --------
-   [⊢ res-e #;#,(substs #'(e_arg- ...) #'(x ...) #'e) ⇒ τ_out
-            #;#,(substs #'(e_arg- ...) #'(X ...) #'τ_out)]]
-  [(_ e_fn e_arg ... ~!) ≫ ; apply var
-;   #: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_argX- ⇒ 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 (ty-arg ...)
-          (stx-map
-           (λ (t) (ev (substs #'(e_argX- ...) #'(X ...) t)))
-           #'(ty-argX ...))
-   #:with (e_arg- ...) (stx-map (λ (e t) (assign-type e t)) #'(e_argX- ...) #'(ty-arg ...))
-   #:with (τ_in ... τ_out)
-          (stx-map
-           (λ (t) (ev (substs #'(e_arg- ...) #'(X ...) t)))
-           #'(τ_inX ... τ_outX))
-   ;; #: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- ...) ⇒ τ_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)
-     #'(define-syntax- alias
-         (make-variable-like-transformer #'τ))]
-    #;[(_ (f:id x:id ...) ty)
-     #'(define-syntax- (f stx)
-         (syntax-parse stx
-           [(_ x ...)
-            #:with τ:any-type #'ty
-            #'τ.norm]))]))
-
-(define-typed-syntax define
-  #;[(_ x:id (~datum :) τ:type e:expr) ≫
-   ;[⊢ e ≫ e- ⇐ τ.norm]
-   #:with y (generate-temporary #'x)
-   --------
-   [≻ (begin-
-        (define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
-        (define- y (ann e : τ.norm)))]]
-  [(_ x:id e) ≫
-   ;This won't work with mutually recursive definitions
-   [⊢ e ≫ e- ⇒ _]
-   #:with y (generate-temporary #'x)
-   #:with y+props (transfer-props #'e- #'y #:except '(origin))
-   --------
-   [≻ (begin-
-        (define-syntax x (make-rename-transformer #'y+props))
-        (define- y e-))]]
-  #;[(_ (f [x (~datum :) ty] ... (~or (~datum →) (~datum ->)) ty_out) e ...+) ≫
-   #:with f- (add-orig (generate-temporary #'f) #'f)
-   --------
-   [≻ (begin-
-        (define-syntax- f
-          (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
-        (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
deleted file mode 100644
index d58f0d6..0000000
--- a/turnstile/examples/tests/dep-peano.rkt
+++ /dev/null
@@ -1,53 +0,0 @@
-#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)
-
-;; TODO: implement nat-ind reductions
-;; 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
deleted file mode 100644
index 87d323e..0000000
--- a/turnstile/examples/tests/dep-tests.rkt
+++ /dev/null
@@ -1,147 +0,0 @@
-#lang s-exp "../dep.rkt"
-(require "rackunit-typechecking.rkt")
-
-; Π → λ ∀ ≻ ⊢ ≫ ⇒
-
-;; examples from Prabhakar's Proust paper
-
-(check-type (λ ([x : *]) x) : (Π ([x : *]) *))
-(typecheck-fail ((λ ([x : *]) x) (λ ([x : *]) x))
- #:verb-msg "expected *, given (Π ([x : *]) *)")
-
-;; transitivity of implication
-(check-type (λ ([A : *][B : *][C : *])
-              (λ ([f : (→ B C)])
-                (λ ([g : (→ A B)])
-                  (λ ([x : A])
-                    (f (g x))))))
-            : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C)))))
-; unnested
-(check-type (λ ([A : *][B : *][C : *])
-              (λ ([f : (→ B C)][g : (→ A B)])
-                (λ ([x : A])
-                  (f (g x)))))
-            : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C))))
-;; no annotations
-(check-type (λ (A B C)
-              (λ (f) (λ (g) (λ (x)
-                (f (g x))))))
-            : (∀ (A B C) (→ (→ B C) (→ (→ A B) (→ A C)))))
-(check-type (λ (A B C)
-              (λ (f g)
-                (λ (x)
-                  (f (g x)))))
-            : (∀ (A B C) (→ (→ B C) (→ A B) (→ A C))))
-;; TODO: partial annotations
-
-;; booleans -------------------------------------------------------------------
-
-;; Bool type
-(define-type-alias Bool (∀ (A) (→ A A A)))
-
-;; Bool terms
-(define T (λ ([A : *]) (λ ([x : A][y : A]) x)))
-(define F (λ ([A : *]) (λ ([x : A][y : A]) y)))
-(check-type T : Bool)
-(check-type F : Bool)
-(define and (λ ([x : Bool][y : Bool]) ((x Bool) y F)))
-(check-type and : (→ Bool 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 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 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)))
-
-;((((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))))
-
-;; 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))))