diff --git a/racket-extended-for-implementing-typed-langs.rkt b/racket-extended-for-implementing-typed-langs.rkt
index b3c32c5..9b6c32a 100644
--- a/racket-extended-for-implementing-typed-langs.rkt
+++ b/racket-extended-for-implementing-typed-langs.rkt
@@ -54,6 +54,15 @@
   ;; (ie where the type rules are declared)
   ;; - matches type vars
   (define-syntax-class meta-term #:datum-literals (:)
+    ;; cases
+    (pattern (name:id e_test [Cons:id (x:id ...) body ...+] ...+ (~optional (~and ldots (~literal ...))))
+     #:with (~datum cases) #'name
+     #:attr args-pat/notypes (template (e_test [Cons (x ...) body ...] ... (?? ldots)))
+     #:attr typevars-pat #'())
+    ;; define-type
+    (pattern (name:id τ_name:id τ_body)
+     #:attr args-pat/notypes #'()
+     #:attr typevars-pat #'(τ_name τ_body))
     ;; define-like binding form
     (pattern (name:id (f:id [x:id : τ] ... (~optional (~and ldots (~literal ...)))) : τ_result e ...)
      #:attr args-pat/notypes (template ((f x ... (?? ldots)) e ...))
@@ -81,6 +90,27 @@
   ;; - matches concrete types
   ;; name identifier is the extended form
   (define-syntax-class term #:datum-literals (:)
+    ;; cases
+    (pattern (name:id e_test [Cons:id (x:id ...) body ...+] ...+)
+     #:with (~datum cases) #'name
+     #:with e_test+ (expand/df #'e_test)
+     #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
+     #:with ((τ ... → τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
+     #:with ((lam (x+ ...) body+ ... body_result+) ...) 
+            (stx-map (λ (bods xs τs) 
+                       (with-extended-type-env 
+                        (stx-map list xs τs)
+                        (expand/df #`(λ #,xs #,@bods))))
+                     #'((body ...) ...)
+                     #'((x ...) ...)
+                     #'((τ ...) ...))
+     #:attr expanded-args #'(e_test+ [Cons+ (x+ ...) body+ ... body_result+] ...)
+     #:attr types #'())
+    ;; define-type
+    (pattern (name:id τ_name:id τ_body)
+     ;;don't expand
+     #:attr expanded-args #'()
+     #:attr types #'(τ_name τ_body))
     ;; define-like binding form
     (pattern (name:id (f:id [x:id : τ] ...) : τ_result e ...)
 ;     #:with (lam xs+ . es+) (with-extended-type-env #'([x τ] ...)
@@ -89,6 +119,7 @@
 ;     #:with es++ (with-extended-type-env #'([x τ] ...)
 ;                  (stx-map (λ (e) (if (identifier? e) (expand/df e) e)) #'es+))
 ;     #:attr expanded-args #'(xs+ . es++)
+     ;; don't expand
      #:attr expanded-args #'((f x ...) e ...)
      #:attr types #'(τ_result τ ...))
     ;; lambda-like binding form
@@ -126,7 +157,11 @@
   ;; **syntax-class: τ-constraint ----------------------------------------
   (define-splicing-syntax-class 
     τ-constraint 
-    #:datum-literals (:= : let typeof == Γ-extend)
+    #:datum-literals (:= : let typeof == Γ-extend with when:)
+    (pattern (when: e)
+     #:attr pattern-directive #'(#:when e))
+    (pattern (with pat e)
+     #:attr pattern-directive #'(#:with pat e))
     (pattern (let τ := (typeof e))
      #:attr pattern-directive #'(#:with τ (typeof #'e)))
     (pattern (e : τ)
@@ -138,6 +173,8 @@
     (pattern (Γ-extend [f : τ] ... (~optional (~and ldots (~literal ...))))
      #:attr pattern-directive
             #`(#:when (Γ (type-env-extend #'([f τ] ... #,@(template ((?? ldots))))))))
+    (pattern (~seq (let τ := (typeof e)) (~literal ...))
+     #:attr pattern-directive #'(#:with (τ (... ...)) (stx-map typeof #'(e (... ...)))))
     (pattern (~seq (e0 : τ0) (~literal ...))
      #:when (concrete-τ? #'τ0)
      #:attr pattern-directive #'(#:when (stx-andmap (λ (e) (assert-type e #'τ0)) #'(e0 (... ...)))))
@@ -156,24 +193,23 @@
      #:with fresh-name (generate-temporary #'meta-e.name)
 ;     #:when (free-id-table-set! defined-names #'meta-e.name #'fresh-name)
      #:with lits lit-set
-     (template
-      (begin
-        (provide (rename-out [fresh-name meta-e.name]))
-        (define-syntax (fresh-name stx)
-          (syntax-parse stx #:literals lits
-            [e:term
-             ;; shadow pattern vars representing subterms with its expansion
-             ;; - except for the name of the form, since result must use base form
-             #:with meta-e.args-pat/notypes #'e.expanded-args
-             #:with meta-e.typevars-pat #'e.types
-             (?? (?@ . ((?@ . c.pattern-directive) ...)))
+     #`(begin
+         (provide (rename-out [fresh-name meta-e.name]))
+         (define-syntax (fresh-name stx)
+           (syntax-parse stx #:literals lits
+             [e:term
+              ;; shadow pattern vars representing subterms with its expansion
+              ;; - except for the name of the form, since result must use base form
+              #:with meta-e.args-pat/notypes #'e.expanded-args
+              #:with meta-e.typevars-pat #'e.types
+              #,@(template ((?? (?@ . ((?@ . c.pattern-directive) ...)))))
              (⊢ (syntax/loc 
                   stx 
-                  (?? expanded-e
-                      (meta-e.name . meta-e.args-pat/notypes)))
+                  #,@(template ((?? expanded-e
+                                    (meta-e.name . meta-e.args-pat/notypes)))))
                 #'meta-τ)]
             [_ #:when (type-error #:src stx #:msg "type error") #'(void)]
-            ))))]))
+            )))]))
 
 
 ;; overload mod-begin to check for define-literal-type-rule and other top-level forms
diff --git a/stlc+define+cons-via-racket-extended-tests.rkt b/stlc+define+cons-via-racket-extended-tests.rkt
index e1a3087..cf1904f 100644
--- a/stlc+define+cons-via-racket-extended-tests.rkt
+++ b/stlc+define+cons-via-racket-extended-tests.rkt
@@ -128,55 +128,55 @@
 (define (ff [x : Int]) : Int (ff x))
 
 ;; define-type (non parametric)
-;(define-type MaybeInt (variant (None) (Just Int)))
-;(check-type (None) : MaybeInt)
-;(check-type (Just 10) : MaybeInt)
-;(check-type-error (Just "ten"))
-;(check-type-error (Just (None)))
-;(define (maybeint->bool [maybint : MaybeInt]) : Bool
-;  (cases maybint
-;   [None () #f]
-;   [Just (x) #t]))
-;(check-type-and-result (maybeint->bool (None)) : Bool => #f)
-;(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
-;(check-type-error (maybeint->bool 25))
-;(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
-;                    (cases maybint
-;                      [None () #f]
-;                      [Just (x) x])))
-;
-;(define-type IntList (variant (Null) (Cons Int IntList)))
-;(check-type-and-result (Null) : IntList => (Null))
-;(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
-;(check-type-error (Cons "one" (Null)))
-;(check-type-error (Cons 1 2))
-;(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
-;  (cases lst
-;    [Null () (Null)]
-;    [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
-;(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
-;(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
-;(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null)))) 
-;                       : IntList => (Cons 3 (Cons 2 (Null))))
-;(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
-;(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
-;(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
-;  (cases lst
-;    [BoolNull () (Null)]
-;    [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
-;(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
-;(check-type-and-result 
-; (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
-; : IntList => (Cons 1 (Null)))
-;(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
-;;; check typename is available
-;(check-type (λ ([lst : IntList]) 
-;              (cases lst
-;                [Null () (None)]
-;                [Cons (x xs) (Just x)]))
-;            : (IntList → MaybeInt))
-;(check-type ((λ ([lst : IntList]) 
-;              (cases lst
-;                [Null () (None)]
-;                [Cons (x xs) (Just x)]))
-;             (Null)) : MaybeInt)
\ No newline at end of file
+(define-type MaybeInt (variant (None) (Just Int)))
+(check-type (None) : MaybeInt)
+(check-type (Just 10) : MaybeInt)
+(check-type-error (Just "ten"))
+(check-type-error (Just (None)))
+(define (maybeint->bool [maybint : MaybeInt]) : Bool
+  (cases maybint
+   [None () #f]
+   [Just (x) #t]))
+(check-type-and-result (maybeint->bool (None)) : Bool => #f)
+(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
+(check-type-error (maybeint->bool 25))
+(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
+                    (cases maybint
+                      [None () #f]
+                      [Just (x) x])))
+
+(define-type IntList (variant (Null) (Cons Int IntList)))
+(check-type-and-result (Null) : IntList => (Null))
+(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
+(check-type-error (Cons "one" (Null)))
+(check-type-error (Cons 1 2))
+(define (map/IntList [f : (Int → Int)] [lst : IntList]) : IntList
+  (cases lst
+    [Null () (Null)]
+    [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
+(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
+(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
+(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null)))) 
+                       : IntList => (Cons 3 (Cons 2 (Null))))
+(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
+(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
+(define (map/BoolList [f : (Bool → Int)] [lst : BoolList]) : IntList
+  (cases lst
+    [BoolNull () (Null)]
+    [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
+(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
+(check-type-and-result 
+ (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
+ : IntList => (Cons 1 (Null)))
+(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
+;; check typename is available
+(check-type (λ ([lst : IntList]) 
+              (cases lst
+                [Null () (None)]
+                [Cons (x xs) (Just x)]))
+            : (IntList → MaybeInt))
+(check-type ((λ ([lst : IntList]) 
+              (cases lst
+                [Null () (None)]
+                [Cons (x xs) (Just x)]))
+             (Null)) : MaybeInt)
\ No newline at end of file
diff --git a/stlc+define+cons-via-racket-extended.rkt b/stlc+define+cons-via-racket-extended.rkt
index 638aa3a..cb6a783 100644
--- a/stlc+define+cons-via-racket-extended.rkt
+++ b/stlc+define+cons-via-racket-extended.rkt
@@ -1,6 +1,7 @@
 #lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
 (extends "stlc-via-racket-extended.rkt" λ)
 (inherit-types Int →)
+(require (for-syntax syntax/stx) "typecheck.rkt")
 
 ;(require "stlc-via-racket-extended.rkt")
 ;(provide Int → + λ #%app #%top-interaction #%module-begin)
@@ -72,6 +73,15 @@
      #:when (Γ (type-env-extend #'([Cons (τ_fld ... → τ)])))
      #'(begin 
          (struct Cons (x ...) #:transparent))]))
+
+(define-typed-syntax
+  (define-type τ (variant (Cons τ_fld ...) ...)) : Unit
+  #:where
+  (Γ-extend [Cons : (τ_fld ... → τ)] ...)
+  (with (flds ...) (stx-map generate-temporaries #'((τ_fld ...) ...)))
+  #:expanded
+  (begin (struct Cons flds #:transparent) ...))
+
 #;(define-syntax/type-rule #:keywords (variant)
   [(define-type τ (variant (Cons τ_fld ...) ...))
    #:where
@@ -101,6 +111,22 @@
                         (cdr (syntax->list #'(τ_result ...)))))
      (⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
         (car (syntax->list #'(τ_result ...))))]))
+(define-typed-syntax
+  (cases e_test [Cons (x ...) e_body ... e_result] ...) : τ_res
+  #:where
+;  (e_body : Unit) ... ...
+  (let (τ ... → τ_Cons) := (typeof Cons)) ...
+  (when: (or (null? (syntax->list #'(τ_Cons ...)))
+             (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_Cons ...)))))
+                     (cdr (syntax->list #'(τ_Cons ...))))))
+  (when: (assert-type #'e_test (stx-car #'(τ_Cons ...))))
+  (let τ_result := (typeof e_result)) ...
+  (when: (or (null? (syntax->list #'(τ_result ...)))
+             (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
+                     (cdr (syntax->list #'(τ_result ...))))))
+  (with τ_res (stx-car #'(τ_result ...)))
+  #:expanded
+  (match e_test [(Cons x ...) e_body ... e_result] ...))
 
 ;; typed forms ----------------------------------------------------------------
 #;(define-syntax (datum/tc stx)