diff --git a/collects/tests/typed-scheme/succeed/simple-or.ss b/collects/tests/typed-scheme/succeed/simple-or.ss
index 3e1cf4c0..51148d2c 100644
--- a/collects/tests/typed-scheme/succeed/simple-or.ss
+++ b/collects/tests/typed-scheme/succeed/simple-or.ss
@@ -5,4 +5,7 @@
 
 ;(let ([tmp (number? x)]) (if tmp tmp (string? x)))
 
-(if (let ([tmp (number? x)]) (if tmp tmp (string? x))) (f x) 0)
\ No newline at end of file
+(if (let ([tmp (number? x)]) 
+      (if tmp tmp (string? x)))
+    (f x)
+    0)
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss
index 9b4a315d..b624179e 100644
--- a/collects/typed-scheme/typecheck/tc-envops.ss
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@@ -65,8 +65,8 @@
 ;; sets the flag box to #f if anything becomes (U)
 (d/c (env+ env fs flag)
   (env? (listof Filter/c) (box/c #t). -> . env?)
-  (define-values (imps atoms) (combine-props fs (env-props env) flag))
-  (for/fold ([Γ (replace-props env imps)]) ([f atoms])
+  (define-values (props atoms) (combine-props fs (env-props env) flag))
+  (for/fold ([Γ (replace-props env (append atoms props))]) ([f atoms])
     (match f
       [(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
       [(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index dce2fb20..87bbf895 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -4,7 +4,7 @@
 (require (rename-in "../utils/utils.ss" [private private-in]))
 (require syntax/kerncase mzlib/trace
          scheme/match (prefix-in - scheme/contract)
-         "signatures.ss" "tc-envops.ss" "tc-metafunctions.ss"
+         "signatures.ss" "tc-envops.ss" "tc-metafunctions.ss" "tc-subst.ss"
          (types utils convenience union subtype remove-intersect type-table)
          (private-in parse-type type-annotation)
          (rep type-rep)
@@ -12,7 +12,7 @@
          (except-in (utils tc-utils stxclass-util))
          (env lexical-env)
          (only-in (env type-environments) lookup current-tvars extend-env)
-         racket/private/class-internal
+         racket/private/class-internal unstable/debug
          (except-in syntax/parse id)
          (only-in srfi/1 split-at))
 
@@ -158,65 +158,83 @@
 ;;                   (Results Results -> Result)
 ;;                   (Type Results -> Type)
 ;;                   (Type Type -> Type))
-(define (check-below tr1 expected)
-  (match* (tr1 expected)
-    ;; these two have to be first so that errors can be allowed in cases where multiple values are expected
-    [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
-     (ret ts2)]
-    [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
-     expected]
-    
-    [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
-     (unless (= (length ts) (length ts2))
-       (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
-     (unless (for/and ([t ts] [s ts2]) (subtype t s))
-       (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
-     (if (= (length ts) (length ts2))
-         (ret ts2 fs os)
-         (ret ts2))]
-    [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
-     (cond 
-       [(not (subtype t1 t2))
-        (tc-error/expr "Expected ~a, but got ~a" t2 t1)])
-     expected]
-    [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
-     (cond 
-       [(not (subtype t1 t2))
-        (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
-       [(and (not (filter-equal? f1 f2))
-             (object-equal? o1 o2))
-        (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
-       [(not (and (equal? f1 f2) (equal? o1 o2)))
-        (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
-     expected]
-    [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
-     (unless (andmap subtype t1 t2)
-       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
-     expected]
-    [((tc-results: t1 fs os) (tc-results: t2 fs os))
-     (unless (= (length t1) (length t2))
-       (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
-     (unless (for/and ([t t1] [s t2]) (subtype t s))
-       (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
-     expected]
-    [((tc-result1: t1 f o) (? Type? t2))
-     (unless (subtype t1 t2)
-       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-     (ret t2 f o)]
-    [((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
-     (unless (subtype t1 t2)
-       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-     t1]
-    [((? Type? t1) (tc-result1: t2 f o))
-     (if (subtype t1 t2)
-         (tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
+(define (check-below tr1 expected)     
+  (define (maybe-abstract r)
+    (define l (hash-ref to-be-abstr expected #f))
+    (define (sub-one proc i)
+      (for/fold ([s i])
+        ([nm (in-list l)])
+        (proc s nm (make-Empty) #t)))
+    (define (subber proc lst)
+      (for/list ([i (in-list lst)])
+        (sub-one proc i)))
+    (if l
+        (match r
+          [(tc-results: ts fs os) 
+           (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
+          [(tc-results: ts fs os dt db) 
+           (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]
+          [t (sub-one subst-type t)])
+        r))
+  (let ([tr1 (debug maybe-abstract tr1)])
+    (match* (tr1 expected)
+      ;; these two have to be first so that errors can be allowed in cases where multiple values are expected
+      [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
+       (ret ts2)]
+      [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
+       expected]
+      
+      [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
+       (unless (= (length ts) (length ts2))
+         (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
+       (unless (for/and ([t ts] [s ts2]) (subtype t s))
+         (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
+       (if (= (length ts) (length ts2))
+           (ret ts2 fs os)
+           (ret ts2))]
+      [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
+       (cond 
+         [(not (subtype t1 t2))
+          (tc-error/expr "Expected ~a, but got ~a" t2 t1)])
+       expected]
+      [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
+       (cond 
+         [(not (subtype t1 t2))
+          (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
+         [(and (not (filter-equal? f1 f2))
+               (object-equal? o1 o2))
+          (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
+         [(not (and (equal? f1 f2) (equal? o1 o2)))
+          (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
+       expected]
+      [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
+       (unless (andmap subtype t1 t2)
+         (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+       expected]
+      [((tc-results: t1 fs os) (tc-results: t2 fs os))
+       (unless (= (length t1) (length t2))
+         (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
+       (unless (for/and ([t t1] [s t2]) (subtype t s))
+         (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
+       expected]
+      [((tc-result1: t1 f o) (? Type? t2))
+       (unless (subtype t1 t2)
          (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-     t1]
-    [((? Type? t1) (? Type? t2))
-     (unless (subtype t1 t2)
-       (tc-error/expr "Expected ~a, but got ~a" t2 t1))
-     expected]
-    [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
+       (ret t2 f o)]
+      [((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
+       (unless (subtype t1 t2)
+         (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+       t1]
+      [((? Type? t1) (tc-result1: t2 f o))
+       (if (subtype t1 t2)
+           (tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
+           (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+       t1]
+      [((? Type? t1) (? Type? t2))
+       (unless (subtype t1 t2)
+         (tc-error/expr "Expected ~a, but got ~a" t2 t1))
+       expected]
+      [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)])))
 
 (define (tc-expr/check/type form expected)
   #;(syntax? Type/c . -> . tc-results?)
diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss
index 86b06ae2..938feeab 100644
--- a/collects/typed-scheme/typecheck/tc-if.ss
+++ b/collects/typed-scheme/typecheck/tc-if.ss
@@ -44,10 +44,16 @@
      (let*-values ([(flag+ flag-) (values (box #t) (box #t))])
        (match-let* ([env-thn (env+ (lexical-env) (list fs+) flag+)]
                     [env-els (env+ (lexical-env) (list fs-) flag-)]
-                    [new-thn-props (env-props env-thn)]
-                    [new-els-props (env-props env-els)]
+                    [new-thn-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env))))))
+                                           (env-props env-thn))]
+                    [new-els-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env)))))) 
+                                           (env-props env-els))]
                     [(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))]
                     [(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))])
+         ;(printf "old thn-props: ~a\n" (env-props (lexical-env)))
+         ;(printf "fs+: ~a~n" fs+)
+         ;(printf "thn-props: ~a~n" (env-props env-thn))
+         ;(printf "new-thn-props: ~a~n" new-thn-props)
          ;; if we have the same number of values in both cases
          (cond [(= (length ts) (length us))
                 (let ([r (combine-results
@@ -59,12 +65,12 @@
                                      [(_ (NoFilter:))
                                       (-FS -top -top)]
                                      [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
-                                      (-FS (-or (-and fs+ f2+) (-and fs- f3+))
-                                           (-or (-and fs+ f2-) (-and fs- f3-)))])]
+                                      (-FS (-or (apply -and fs+ f2+ new-thn-props) (-and fs- f3+))
+                                           (-or (apply -and fs+ f2- new-thn-props) (-and fs- f3-)))])]
                                   [type (Un t2 t3)]
                                   [object (if (object-equal? o2 o3) o2 (make-Empty))])
                               ;(printf "result filter is: ~a\n" filter)
-                              (debug ret type filter object))))])
+                              (ret type filter object))))])
                   (if expected (check-below r expected) r))]
                ;; special case if one of the branches is unreachable
                [(and (= 1 (length us)) (type-equal? (car us) (Un)))
diff --git a/collects/typed-scheme/typecheck/tc-let-unit.ss b/collects/typed-scheme/typecheck/tc-let-unit.ss
index aea276ff..763841a0 100644
--- a/collects/typed-scheme/typecheck/tc-let-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-let-unit.ss
@@ -1,7 +1,7 @@
 #lang scheme/unit
 
 (require (rename-in "../utils/utils.ss" [infer r:infer]))
-(require "signatures.ss" "tc-metafunctions.ss"
+(require "signatures.ss" "tc-metafunctions.ss" "tc-subst.ss"
          (types utils convenience)
          (private type-annotation parse-type)
 	 (env lexical-env type-alias-env type-env type-environments)
@@ -36,11 +36,12 @@
               (match r 
                 [(tc-results: ts (FilterSet: fs+ fs-) os) 
                  (values ts
-                         (for/list ([n names]
-                                    [f+ fs+]
-                                    [f- fs-])
-                           (-and (make-ImpFilter (make-NotTypeFilter (-val #f) null n) f+)
-                                 (make-ImpFilter (make-TypeFilter (-val #f) null n) f-))))]))))
+                         (apply append
+                                (for/list ([n names]
+                                           [f+ fs+]
+                                           [f- fs-])
+                                  (list (make-ImpFilter (make-NotTypeFilter (-val #f) null n) f+)
+                                        (make-ImpFilter (make-TypeFilter (-val #f) null n) f-)))))]))))
      ;; extend the lexical environment for checking the body
   (with-lexical-env/extend/props
    ;; the list of lists of name
@@ -49,14 +50,29 @@
    types
    (w/c append-region
     #:result (listof Filter?)
-    (append (apply append props) (env-props (lexical-env))))
+    (define-values (p1 p2)
+      (combine-props (apply append props) (env-props (lexical-env)) (box #t)))
+    (append p1 p2))
    (for-each expr->type
              clauses
              exprs 
              results)
-   (if expected 
-       (tc-exprs/check (syntax->list body) expected)
-       (tc-exprs (syntax->list body)))))
+   (let ([subber (lambda (proc lst)
+                   (for/list ([i (in-list lst)])
+                     (for/fold ([s i])
+                       ([nm (in-list (apply append namess))])
+                       (proc s nm (make-Empty) #t))))])
+     (if expected 
+         (begin
+           (hash-update! to-be-abstr expected
+                         (lambda (old-l) (apply append old-l namess))
+                         null)
+           (tc-exprs/check (syntax->list body) expected))
+         (match (tc-exprs (syntax->list body))           
+           [(tc-results: ts fs os)
+            (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
+           [(tc-results: ts fs os dt db)
+            (ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)])))))
 
 (define (tc/letrec-values/check namess exprs body form expected)
   (tc/letrec-values/internal namess exprs body form expected))
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 3cb72f67..e2a58916 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -7,6 +7,7 @@
                     [one-of/c -one-of/c])
          (rep type-rep filter-rep rep-utils) scheme/list
          scheme/contract scheme/match unstable/match scheme/trace
+         unstable/debug
          (for-syntax scheme/base))
 
 ;(provide (all-defined-out))
@@ -125,6 +126,7 @@
           (match p      
             [(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))]
             [(ImpFilter: a c)
+             ;(printf "combining ~a with ~a\n" p (append derived-props derived-atoms))
              (if (for/or ([p (append derived-props derived-atoms)])
                    (implied-atomic? a p))
                  (loop derived-props derived-atoms (cons c (cdr worklist)))
diff --git a/collects/typed-scheme/typecheck/tc-subst.ss b/collects/typed-scheme/typecheck/tc-subst.ss
index 468328c1..c52427f5 100644
--- a/collects/typed-scheme/typecheck/tc-subst.ss
+++ b/collects/typed-scheme/typecheck/tc-subst.ss
@@ -6,7 +6,7 @@
                     [->* -->*]
                     [one-of/c -one-of/c])
          (rep type-rep filter-rep rep-utils) scheme/list
-         scheme/contract scheme/match unstable/match
+         scheme/contract scheme/match unstable/match unstable/debug
          (for-syntax scheme/base)
          "tc-metafunctions.ss")
 
@@ -16,6 +16,12 @@
   (begin (d/c (name . args) c . body)
          (p/c [name c])))
 
+(define (name-ref=? a b)
+  (or (eq? a b)
+      (and (identifier? a)
+           (identifier? b)
+           (free-identifier=? a b))))
+
 (d/c/p (open-Result r objs)
        (-> Result? (listof Object?) (values Type/c FilterSet? Object?))
        (match r
@@ -27,14 +33,14 @@
                     (subst-object old-obj k o #t)))]))
 
 (d/c/p (subst-filter-set fs k o polarity)
-       (-> FilterSet? integer? Object? boolean? FilterSet?)
+       (-> FilterSet? name-ref/c Object? boolean? FilterSet?)
   (match fs
     [(FilterSet: f+ f-)
      (combine (subst-filter f+ k o polarity) 
 	      (subst-filter f- k o polarity))]))
 
-(d/c (subst-type t k o polarity)
-     (-> Type/c integer? Object? boolean? Type/c)
+(d/c/p (subst-type t k o polarity)
+     (-> Type/c name-ref/c Object? boolean? Type/c)
   (define (st t) (subst-type t k o polarity))
   (d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
   (type-case (#:Type st 
@@ -44,20 +50,22 @@
               [#:arr dom rng rest drest kws
                      ;; here we have to increment the count for the domain, where the new bindings are in scope
                      (let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
-                            [st* (lambda (t) (subst-type t (+ arg-count k) o polarity))])
+                            [st* (if (integer? k)
+                                     (λ (t) (subst-type t (+ arg-count k) o polarity))
+                                     st)])
                        (make-arr (map st dom)
                                  (st* rng)
                                  (and rest (st rest))
                                  (and drest (cons (st (car drest)) (cdr drest)))
                                  (map st kws)))]))
 
-(d/c (subst-object t k o polarity)
-     (-> Object? integer? Object? boolean? Object?)
+(d/c/p (subst-object t k o polarity)
+     (-> Object? name-ref/c Object? boolean? Object?)
   (match t
     [(NoObject:) t]
     [(Empty:) t]
     [(Path: p i)
-     (if (eq? i k)
+     (if (name-ref=? i k)
 	 (match o
 	   [(Empty:) (make-Empty)]
 	   ;; the result is not from an annotation, so it isn't a NoObject
@@ -67,13 +75,17 @@
 
 ;; this is the substitution metafunction 
 (d/c/p (subst-filter f k o polarity)
-  (-> Filter/c integer? Object? boolean? Filter/c)
-  (define (ap f) (subst-filter f o polarity))
+  (-> Filter/c name-ref/c Object? boolean? Filter/c)
+  (define (ap f) (subst-filter f k o polarity))
   (define (tf-matcher t p i k o polarity maker)
     (match o
-      [(or (Empty:) (NoObject:)) (if polarity -top -bot)]
+      [(or (Empty:) (NoObject:)) 
+       (cond [(name-ref=? i k)
+	      (if polarity -top -bot)]
+	     [(index-free-in? k t) (if polarity -top -bot)]
+             [else f])]
       [(Path: p* i*)
-       (cond [(eq? i k)
+       (cond [(name-ref=? i k)
 	      (maker
 	       (subst-type t k o polarity)
 	       (append p p*) 
@@ -83,8 +95,8 @@
   (match f
     [(ImpFilter: ant consq)
      (make-ImpFilter (subst-filter ant k o (not polarity)) (ap consq))]
-    [(AndFilter: fs) (make-AndFilter (map ap fs))]
-    [(OrFilter: fs) (make-OrFilter (map ap fs))]
+    [(AndFilter: fs) (apply -and (map ap fs))]
+    [(OrFilter: fs) (apply -or (map ap fs))]
     [(Bot:) -bot]
     [(Top:) -top]
     [(TypeFilter: t p i)
@@ -99,7 +111,7 @@
      (object-case (#:Type for-type)
 		  o
 		  [#:Path p i
-			  (if (eq? i k)
+			  (if (name-ref=? i k)
 			      (return #t)
 			      o)]))
    (define (for-filter o)
@@ -107,11 +119,11 @@
 		   #:Filter for-filter)
 		  o
 		  [#:NotTypeFilter t p i
-				   (if (eq? i k)
+				   (if (name-ref=? i k)
 				       (return #t)
 				       o)]
 		  [#:TypeFilter t p i
-				(if (eq? i k)
+				(if (name-ref=? i k)
 				    (return #t)
 				    o)]))
    (define (for-type t)
@@ -128,7 +140,8 @@
                                    (and rest (for-type rest))
                                    (and drest (cons (for-type (car drest)) (cdr drest)))
                                    (map for-type kws)))]))
-   (for-type type)))
+   (for-type type)
+    #f))
 
 ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
 (d/c/p (values->tc-results tc formals)
diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss
index 09ca8fe0..71e2c7f9 100644
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@@ -71,6 +71,9 @@
 
 (define Ident (-Syntax -Symbol))
 
+(define (atomic-filter? e)
+  (or (TypeFilter? e) (NotTypeFilter? e)))
+
 (define (opposite? f1 f2)
   (match* (f1 f2)
           [((TypeFilter: t1 p1 i1)
@@ -124,11 +127,15 @@
            (loop (cdr props) others)]
           [p (loop (cdr props) (cons p others))]))))
 
-(define (-or . args) 
+(define (-or . args)
+  (define mk
+    (case-lambda [() -bot]
+                 [(f) f]
+                 [fs (make-OrFilter fs)]))
   (define (distribute args)
     (define-values (ands others) (partition AndFilter? args))
     (if (null? ands)
-        (make-OrFilter others)
+        (apply mk others)
         (match-let ([(AndFilter: elems) (car ands)])
           (apply -and (for/list ([a (in-list elems)])
                         (apply -or a (append (cdr ands) others)))))))  
@@ -152,7 +159,7 @@
                   (loop (cdr fs) (cons t result))])]))))
 
 (define (-and . args) 
-  (let loop ([fs args] [result null])
+  (let loop ([fs (remove-duplicates args filter-equal?)] [result null])
     (if (null? fs)
         (match result
           [(list) -top]
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index c287b8be..95c07978 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -310,3 +310,10 @@
 ;; a parameter for the current polymorphic structure being defined
 ;; to allow us to prevent non-regular datatypes
 (define current-poly-struct (make-parameter #f))
+
+;; a table indicating what variables should be abstracted away before using this expected type
+;; keyed on the numeric Rep sequence
+(define to-be-abstr
+  (make-weak-hash))
+
+(provide to-be-abstr)
\ No newline at end of file