diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss
new file mode 100644
index 00000000..ba631895
--- /dev/null
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@@ -0,0 +1,44 @@
+#lang scheme/base
+
+(require (rename-in "../utils/utils.ss" [infer infer-in]))
+(require (rename-in (types subtype convenience remove-intersect)                   
+                    [-> -->]
+                    [->* -->*]
+                    [one-of/c -one-of/c])
+         (infer-in infer)
+         (rep type-rep)
+         scheme/contract scheme/match
+         stxclass/util
+         (for-syntax scheme/base))
+
+(define (replace-nth l i f)
+  (cond [(null? l) (error 'replace-nth "list not long enough" l i f)]
+        [(zero? i) (cons (f (car l)) (cdr l))]
+        [else (cons (car l) (replace-nth (cdr l) (sub1 i) f))]))
+
+(define/contract (update t lo)
+  (Type/c Filter/c . -> . Type/c)
+  (match* (t lo)
+    ;; pair ops
+    [((Pair: t s) (TypeFilter: u (list* (CarPE:) rst) x))
+     (make-Pair (update t (make-TypeFilter u rst x)) s)]
+    [((Pair: t s) (NotTypeFilter: u (list* (CarPE:) rst) x))
+     (make-Pair (update t (make-NotTypeFilter u rst x)) s)]
+    [((Pair: t s) (TypeFilter: u (list* (CarPE:) rst) x))
+     (make-Pair t (update s (make-TypeFilter u rst x)))]
+    [((Pair: t s) (NotTypeFilter: u (list* (CdrPE:) rst) x))
+     (make-Pair t (update s (make-NotTypeFilter u rst x)))]
+    
+    ;; struct ops
+    [((Struct: nm par flds proc poly pred cert) 
+      (TypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
+     (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))))]
+    [((Struct: nm par flds proc poly pred cert) 
+      (NotTypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
+     (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))))]
+    
+    ;; otherwise
+    [(t (TypeFilter: u (list) _))
+     (restrict t u)]
+    [(t (NotTypeFilter: u (list) _))
+     (remove t u)]))
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 4081a3ad..96258fd0 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -39,8 +39,8 @@
     (lambda (stx) #'(? (lambda (id) (free-identifier=? id x)))))
   (match f
     [(Bot:) (list (make-LBot))]
-    [(TypeFilter: t p (=x)) (list (make-LTypeFilter t p))]
-    [(NotTypeFilter: t p (=x)) (list (make-LNotTypeFilter t p))]
+    [(TypeFilter: t p (=x)) (list (make-LTypeFilter t p idx))]
+    [(NotTypeFilter: t p (=x)) (list (make-LNotTypeFilter t p idx))]
     [_ null]))
 
 (define/contract (apply-filter lfs t o)
@@ -58,5 +58,32 @@
     [((LNotTypeFilter: (? (lambda (t) (subtype s t))) (list) _) _ _) (list (make-Bot))]
     [((LTypeFilter: (? (lambda (t) (not (overlap s t)))) (list) _) _ _) (list (make-Bot))]
     [(_ _ (Empty:)) null]
-    [((LTypeFilter: t pi* _) _ (Path: pi x)) (make-TypeFilter t (append pi* pi) x)]
-    [((LNotTypeFilter: t pi* _) _ (Path: pi x)) (make-NotTypeFilter t (append pi* pi) x)]))
\ No newline at end of file
+    [((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))]
+    [((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
+
+(define-match-expander T-FS:
+  (lambda (stx) #'(FilterSet: _ (list (Bot:)))))
+(define-match-expander F-FS:
+  (lambda (stx) #'(FilterSet: (list (Bot:)) _)))
+
+(define/contract (combine-filter f1 f2 f3)
+  (FilterSet? FilterSet? FilterSet? . -> . FilterSet?)
+  (match* (f1 f2 f3)
+    [(f (T-FS:) (F-FS:)) f] ;; the student expansion
+    [((T-FS:) f _) f]
+    [((F-FS:) _ f) f]
+    ;; skipping the general or/predicate rule because it's really complicated
+    ;; or/predicate special case for one elem lists
+    ;; note that we are relying on equal? on identifiers here
+    [((FilterSet: (list (TypeFilter: t pi x)) (list (NotTypeFilter: t pi x)))
+      (T-FS:)
+      (FilterSet: (list (TypeFilter: s pi x)) (list (NotTypeFilter: s pi x))))
+     (make-FilterSet (list (make-TypeFilter (Un t s) pi x)) (list (make-NotTypeFilter (Un t s) pi x)))]
+    ;; or
+    [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (combine null (append f1- f3-))]
+    ;; and
+    [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) (combine (append f1+ f2+) null)]
+    [(f f* f*) f*]
+    [(_ _ _)
+     ;; could intersect f2 and f3 here
+     (make-FilterSet null null)]))
\ No newline at end of file