diff --git a/graph/graph/cond-abort.rkt b/graph/graph/cond-abort.rkt
new file mode 100644
index 0000000..3aa0907
--- /dev/null
+++ b/graph/graph/cond-abort.rkt
@@ -0,0 +1,92 @@
+#lang typed/racket
+
+(provide cond-abort
+         match-abort)
+
+(define-syntax (cond-abort orig-stx)
+  (let rec ([stx orig-stx])
+    (syntax-case stx (else =>)
+      [(_)
+       #`(typecheck-fail #,orig-stx)]
+      [(_ [else body0 . body])
+       #`(let () body0 . body)]
+      [(_ [condition] . rest)
+       ;; TODO: this does not work when body returns multiple values.
+       #`(let ([result condition])
+           (if (or (not result) (eq? result 'continue))
+               #,(rec #'(cond-abort . rest))
+               (if (eq? result 'break)
+                   'continue
+                   result)))]
+      [(_ [condition body0 . body] . rest)
+       ;; TODO: this does not work when body returns multiple values.
+       #`(let ([result (if condition
+                           (let () body0 . body)
+                           'continue)])
+           (if (eq? result 'continue)
+               #,(rec #'(cond-abort . rest))
+               (if (eq? result 'break)
+                   'continue
+                   result)))])))
+
+(define-syntax-rule (match-abort v [pattern body0 . body] ...)
+  (let ([v-cache v])
+    (cond-abort
+     [#t (match v-cache
+           [pattern (let () body0 . body)]
+           [_ 'continue])]
+     ...)))
+
+(module* test typed/racket
+  (require typed/rackunit)
+  (require (submod ".."))
+  
+  ;; Type Checker: Incomplete case coverage in: (cond-abort)
+  ;(cond-abort)
+  
+  (check-equal? (cond-abort [else 1]) 1)
+  (check-equal? (cond-abort [#f 0] [else 1]) 1)
+  
+  (check-equal? (cond-abort [#t 2]) 2)
+  (check-equal? (cond-abort [#f 0] [#t 2]) 2)
+  
+  (check-equal? (cond-abort [#t 'continue]
+                            [#f (typecheck-fail #'"We should never get here")]
+                            [#t 3])
+                3)
+  
+  (check-equal?
+   (cond-abort
+    [#t 'continue]
+    [#t (let ([ret (cond-abort
+                    [#t 'continue]
+                    [#f (typecheck-fail #'"We should never get here")]
+                    [#t 'break]
+                    [#t (typecheck-fail #'"We should never get here")]
+                    [#t 'continue]
+                    [#t (typecheck-fail #'"We should never get here")])])
+          (ann ret 'continue))]
+    [#t 4])
+   4)
+  
+  (check-equal?
+   (ann (let ([f (λ ([x : Integer])
+                   (cond-abort
+                    [#t (if (< x 3) 'continue x)]
+                    [#f (typecheck-fail #'"We should never get here")]
+                    [#t 4]
+                    [else (typecheck-fail #'"We should never get here")]))])
+          (list (f 2) (f 7)))
+        (Listof Positive-Integer))
+   '(4 7))
+  
+  (check-equal?
+   (match-abort '(1 2 3)
+     [(cons a b)
+      (match-abort b
+        [(list x y z) 'one]
+        [(cons x y) 'break]
+        [_ (typecheck-fail #'"We should never get here")])]
+     [(list a b c)
+      'two])
+   'two))
\ No newline at end of file
diff --git a/graph/graph/rewrite-type.lp2.rkt b/graph/graph/rewrite-type.lp2.rkt
index 1089b04..bb82e18 100644
--- a/graph/graph/rewrite-type.lp2.rkt
+++ b/graph/graph/rewrite-type.lp2.rkt
@@ -10,13 +10,18 @@ result.
 
 For example, one could replace all strings in a data structure by their length:
 
-@chunk[<test-example>
-       'a
+@CHUNK[<test-example>
        (begin-for-syntax 
+         #;(displayln
+          (syntax->datum
+           (replace-in-instance #'(List (Pairof (Vector Symbol
+                                                              (Vectorof String))
+                                                      String))
+                                      #'([String Number string-length]))))
          (displayln
           (syntax->datum
-           (replace-in-data-structure #'(List (Pairof Symbol String))
-                                      #'([String Number string-length])))))
+           (replace-in-instance #'(List Symbol String)
+                                     #'([String Number string-length])))))
        #;(define-syntax (string→number stx)
            (replace-in-data-structure
             #'(List (Pairof Symbol String))
@@ -24,20 +29,75 @@ For example, one could replace all strings in a data structure by their length:
 
 @CHUNK[<replace-in-data-structure>
        (define-for-syntax (replace-in-data-structure t r)
+         (define (recursive-replace new-t) (replace-in-data-structure new-t r))
          (define/with-syntax ([from to fun] ...) r)
          (syntax-parse t
            [x:id
-            #:attr assoc-from-to (stx-assoc #'x #'((from . to) ...))
+            #:attr assoc-from-to (cdr-stx-assoc #'x #'((from . to) ...))
             #:when (attribute assoc-from-to)
             #'assoc-from-to]
            [((~literal List) a ...)
-            #`(List #,@(stx-map (λ (x) (replace-in-data-structure x r))
-                                #'(a ...)))]
+            #`(List #,@(stx-map recursive-replace #'(a ...)))]
            [((~literal Pairof) a b)
-            #`(Pairof #,(replace-in-data-structure #'a r)
-                      #,(replace-in-data-structure #'b r))]
+            #`(Pairof #,(recursive-replace #'a) #,(recursive-replace #'b))]
+           [((~literal Listof) a)
+            #`(Listof #,(recursive-replace #'a))]
+           [((~literal Vector) a ...)
+            #`(Vector #,@(stx-map recursive-replace #'(a ...)))]
+           [((~literal Vectorof) a)
+            #`(Vectorof #,(recursive-replace #'a))]
+           [((~literal U) a ...)
+            #`(U #,@(stx-map recursive-replace #'(a ...)))]
            [x:id #'x]))]
 
+@CHUNK[<replace-in-instance>
+       (define-for-syntax (replace-in-instance t r)
+         (define/with-syntax ([from to fun] ...) r)
+         (define (recursive-replace type)
+           (syntax-parse type
+           [x:id
+            #:attr assoc-from-to (cdr-stx-assoc #'x #'((from . (to . fun)) ...))
+            #:when (attribute assoc-from-to)
+            #:with (to-type . to-fun) #'assoc-from-to
+            (define/with-syntax (tmp) (generate-temporaries #'(x)))
+            ;; TODO: Add predicate for to-type in the pattern.
+            (cons #`(and tmp) #`(to-fun tmp))]
+           [((~literal List) a ...)
+            (define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
+            (define rec (stx-map recursive-replace #'(a ...)))
+            (cons #`(list #,@(map car rec))
+                  #`(list #,@(map cdr rec)))]
+           [((~literal Pairof) a b)
+            (define/with-syntax (tmpa tmpb) (generate-temporaries #'(a b)))
+            (define reca (recursive-replace #'a))
+            (define recb (recursive-replace #'b))
+            (cons #`(cons #,(car reca) #,(car recb))
+                  #`(cons #,(cdr reca) #,(cdr recb)))]
+           #| TODO:
+           [((~literal Listof) a)
+            #`(Listof #,(recursive-replace #'x))]
+           [((~literal Vector) a ...)
+            #`(Vector #,@(stx-map recursive-replace #'(a ...)))]
+           [((~literal Vectorof) a)
+            #`(Vectorof #,(recursive-replace #'a))]
+           |#
+           #|
+           [((~literal U) a ...)
+            ;; Use (app (λ _ 'a) U-case) to set U-case, so that we can do a
+            ;; very simple cond in the replacement.
+            ;; TODO: write a `bind` match-expander, much like syntax-parse's
+            ;; ~bind.
+            (define/with-syntax (tmp ...) (generate-temporaries #'(a ...)))
+            (cons #`(or (app (λ _')]
+           ;; DOES NOT ACTUALLY WORK, because match wants all `or` branches to
+           ;; have the same variables.
+           |#
+           [x:id
+            (define/with-syntax (tmp) (generate-temporaries #'(x)))
+            (cons #'tmp #'tmp)]))
+         (define whole-rec (recursive-replace t))
+         #`(λ (v) (match-abort v [#,(car whole-rec) #,(cdr whole-rec)])))]
+
 @chunk[<*>
        (begin
          (module main typed/racket;;;;;;;;;;
@@ -48,10 +108,13 @@ For example, one could replace all strings in a data structure by their length:
                     "structure.lp2.rkt"
                     "variant.lp2.rkt"
                     "../type-expander/multi-id.lp2.rkt"
-                    "../type-expander/type-expander.lp2.rkt")
-           (begin-for-syntax (provide replace-in-data-structure))
+                    "../type-expander/type-expander.lp2.rkt"
+                    "cond-abort.rkt")
+           (begin-for-syntax (provide replace-in-data-structure
+                                      replace-in-instance))
            
-           <replace-in-data-structure>)
+           <replace-in-data-structure>
+           <replace-in-instance>)
          
          (require 'main)
          (provide (all-from-out 'main))
@@ -62,7 +125,8 @@ For example, one could replace all strings in a data structure by their length:
                     "structure.lp2.rkt"
                     "variant.lp2.rkt"
                     "../type-expander/multi-id.lp2.rkt"
-                    "../type-expander/type-expander.lp2.rkt")
+                    "../type-expander/type-expander.lp2.rkt"
+                    "cond-abort.rkt")
            
            <test-example>
            
diff --git a/graph/lib/low.rkt b/graph/lib/low.rkt
index ff27b5b..96c1688 100644
--- a/graph/lib/low.rkt
+++ b/graph/lib/low.rkt
@@ -498,7 +498,7 @@
 
 ;; ==== syntax.rkt ====
 
-(provide stx-assoc)
+(provide stx-assoc cdr-stx-assoc)
 ;(require/typed racket/base [(assoc assoc3) (∀ (a b) (→ Any (Listof (Pairof a b)) (U False (Pairof a b))))])
 (require/typed racket/base
                [(assoc assoc3)
@@ -525,4 +525,14 @@
                         [else e-alist])])
     (assoc3 id e-e-alist free-identifier=?)))
 
+(: cdr-stx-assoc
+   (∀ (T) (→ Identifier
+             (U (Syntaxof (Listof (Syntaxof (Pairof Identifier T))))
+                (Listof (Syntaxof (Pairof Identifier T)))
+                (Listof (Pairof Identifier T)))
+             (U T #f))))
+(define (cdr-stx-assoc id alist)
+  (let ((res (stx-assoc id alist)))
+    (if res (cdr res) #f)))
+
 ;; ==== end ====
\ No newline at end of file