diff --git a/graph/graph/fold-queues.lp2.rkt b/graph/graph/fold-queues.lp2.rkt
index 9178ec6..40126c3 100644
--- a/graph/graph/fold-queues.lp2.rkt
+++ b/graph/graph/fold-queues.lp2.rkt
@@ -12,26 +12,26 @@
 
 @chunk[<fold-queues-signature>
        (fold-queues root-value
-                    [(name [element (~literal :) element-type] Δ-queues enqueue)
+                    [(name [element (~literal :) Element-Type] Δ-queues enqueue)
                      (~literal :) result-type
                      . body]
                     ...)]
 
 @chunk[<define-enqueue-type>
-       (define/with-syntax get-tag/type
-         #'(∀ (X) (case→ (→ 'name element-type X (values Index X))
+       (define/with-syntax enqueue/type
+         #'(∀ (X) (case→ (→ 'name Element-Type X (values Index X))
                          ...)))]
 
 @chunk[<define-Δ-queues-type>
        (define/with-syntax queues/type
-         #'(List (Δ-Hash element-type Index) ...))]
+         #'(List (Δ-Hash Element-Type Index) ...))]
 
 @chunk[<fold-queue-multi-sets-immutable-tags>
        (define-syntax/parse <fold-queues-signature>
          <define-enqueue-type>
          <define-Δ-queues-type>
-         #'(list (λ ([element : element-type]
-                     [enqueue : get-tag/type]
+         #'(list (λ ([element : Element-Type]
+                     [enqueue : enqueue/type]
                      [Δ-queues : queues/type])
                    : result-type
                    . body)
diff --git a/graph/graph/graph2.lp2.rkt b/graph/graph/graph2.lp2.rkt
index 986f5cb..e24268f 100644
--- a/graph/graph/graph2.lp2.rkt
+++ b/graph/graph/graph2.lp2.rkt
@@ -6,6 +6,10 @@
 
 @(table-of-contents)
 
+@; TODO: allow a mapping to return a new placeholder, in order to act as a
+@; redirect. All references to the old placeholder will act as if they were to
+@; the new placeholder.
+
 @section{Introduction}
 
 This module provides a @tc[graph] macro which helps constructing immutable
@@ -18,9 +22,10 @@ name. For example, a graph representing a city and its inhabitants could use
 these variants:
 
 @chunk[<example-variants>
-       [City [streets : (Listof Street)] [inhabitants : (Listof Person)]]
-       [Street [houses : (Listof House)]]
-       [House [owner : Person] [location : Street]]
+       [City #|[streets : (Listof Street)]|# [inhabitants : (Listof Person)]]
+       #|DEBUG|#
+       #|[Street [houses : (Listof House)]]
+       [House [owner : Person] [location : Street]]|#
        [Person [name : String]]]
 
 Notice the cycle in the type: a street contains houses, which are located on the
@@ -53,10 +58,12 @@ Here is the root mapping for our example. It maps over the list of names and
 street names @tc[c], and calls for each element the @tc[street] and @tc[person]
 mappings.
 
+@; Would be nicer with (map (∘ (curry street c) my-car) c)), but that doesn't
+@; typecheck (yet).
 @chunk[<example-mappings>
        [(city [c : (Listof (Pairof String String))]) : City
-        (City (remove-duplicates (map (∘ (curry street c) car) c))
-              (remove-duplicates (map (∘ Person cdr) c)))]]
+        (City #|DEBUG|##|(remove-duplicates (map (curry street c) (cars c)))|#
+         (remove-duplicates (map Person (cdrs c))))]]
 
 @subsubsection{More mappings}
 
@@ -64,11 +71,12 @@ Next, we write the @tc[street] mapping, which takes a street name and the whole
 city @tc[c] in list form, and creates a @tc[Street] node.
 
 @chunk[<example-mappings>
-       [(street [c : (Listof (Pairof String String))] [s : String]) : Street
-        (Street (map (∘ (curry house s c) car)
-                     (filter (λ ([x : (Pairof String String)])
-                               (equal? (cdr x) s))
-                             c)))]]
+       #|DEBUG|#
+       #|[(street [c : (Listof (Pairof String String))] [s : String]) : Street
+       (Street (map (curry (curry house s) c)
+       (cars (filter (λ ([x : (Pairof String String)])
+       (equal? (cdr x) s))
+       c))))]|#]
 
 The @tc[house] mapping calls back the @tc[street] mapping, to store for each
 house a reference to the containing street. Normally, this would cause infinite
@@ -86,9 +94,11 @@ no risk of forcing one before it is available.
 Finally, we write the @tc[house] mapping.
 
 @chunk[<example-mappings>
+       #|
        [(house [s : String] [c : (Listof (Pairof String String))] [p : String])
-        : House
-        (House (Person p) (street c s))]]
+       : House
+       (House (Person p) (street c s))]|#
+       #|DEBUG|#]
 
 Notice how we are calling directly the @tc[Person] constructor above. We also
 called it directly in the @tc[city] mapping. Since @tc[Person] does not contain
@@ -168,12 +178,14 @@ A single node name can refer to several types:
   @racket[[City (Listof Street) (Listof Person)]], it is never used as-is in
   practice}
  @item{The @emph{incomplete} type, in which references to other node types are
-  allowed to be either actual instances, or placeholders. For example,
-  @racket[[City (Listof (U Street Street-Placeholder))
-           (Listof (U Person Person-Placeholder))]].}
+  allowed to be either actual (@racket[incomplete]) instances, or placeholders.
+  For example, @racket[[City (Listof (U Street Street/placeholder-type))
+                        (Listof (U Person Person/placeholder-type))]].}
  @item{The @emph{with-promises} type, in which references to other node types
-  must be replaced by promises for these. For example,
-  @racket[[City (Listof (Promise Street)) (Listof (Promise Person))]].}]
+  must be replaced by a @racket[Promise] for the target node's
+  @racket[with-promises] type. For example,
+  @racket[[City (Listof (Promise Street/with-promises-type))
+           (Listof (Promise Person/with-promises-type))]].}]
 
 When the user code calls a mapping, a placeholder is instead returned. We
 therefore will have one placeholder type per mapping. Mappings come in various
@@ -196,7 +208,7 @@ flexible through wrapper macros.
         (root-expr:expr ...)
         [(mapping:id [param:id (~literal :) param-type:expr] ...)
          (~literal :) result-type:expr
-         . body]
+         . mapping-body]
         ...)]
 
 The macro relies heavily on two sidekick modules: @tc[rewrite-type], and
@@ -279,12 +291,14 @@ tagged with the @tc[mapping]'s name), and a constructor:
 
 @; TODO: just use (variant [mapping param-type ...] ...)
 
-@chunk[<define-placeholder>
-       (define-type mapping/placeholder-type (List 'mapping param-type ...))
+@chunk[<define-mapping-placeholder>
+       (define-type mapping/placeholder-type (List 'placeholder
+                                                   'mapping
+                                                   param-type ...))
        
        (: mapping/make-placeholder (→ param-type ... mapping/placeholder-type))
        (define (mapping/make-placeholder [param : param-type] ...)
-         (list 'mapping param ...))]
+         (list 'placeholder 'mapping param ...))]
 
 The code above needs some identifiers derived from @tc[mapping] names:
 
@@ -303,14 +317,30 @@ that node's @tc[with-promises] type.
 
 @; TODO: use a type-expander here, instead of a template metafunction.
 
-@CHUNK[<define-with-promises>
-       (define-type node/with-promises-type
-         (tmpl-replace-in-type (List 'node field-type ...)
-                               ([node (Promise node/with-promises-type)] ...)))]
+@CHUNK[<define-with-promises-nodes>
+       (define-type field/with-promises-type
+         (tmpl-replace-in-type field-type
+                               [node (Promise node/with-promises-type)]
+                               …))
+       …
+       
+       (define-type node/with-promises-type (List 'with-promises
+                                                  'node
+                                                  field/with-promises-type …))
+       
+       (: node/make-with-promises (→ field/with-promises-type …
+                                     node/with-promises-type))
+       (define (node/make-with-promises field-name …)
+         (list 'with-promises 'node field-name …))]
+
+The code above needs some identifiers derived from @tc[node] and
+@tc[field-name]s:
 
 @chunk[<define-ids>
        (define-temp-ids "~a/make-with-promises" (node ...))
-       (define-temp-ids "~a/with-promises-type" (node ...))]
+       (define-temp-ids "~a/with-promises-type" (node ...))
+       (define/with-syntax ((field/with-promises-type …) …)
+         (stx-map generate-temporaries #'((field-name …) …)))]
 
 @subsection{Making incomplete nodes}
 
@@ -324,31 +354,142 @@ which return type is the desired node type.
 
 @; TODO: use a type-expander here, instead of a template metafunction.
 
-@CHUNK[<define-incomplete>
-       (define-type field/incomplete-type
-         (tmpl-replace-in-type field-type
-                               ([node (U node/incomplete-type
-                                         mapping/placeholder-type ...)] ...)))
-       ...
+@CHUNK[<define-incomplete-nodes>
+       (define-type field/incomplete-type <field/incomplete-type>)
+       …
        
-       (define-type node/incomplete-type (List 'node field/incomplete-type …))
+       (define-type node/incomplete-type
+         (Pairof 'incomplete (Pairof 'node (List field/incomplete-type …))))
        
        (: node/make-incomplete (→ field/incomplete-type … node/incomplete-type))
        (define (node/make-incomplete field-name …)
-         (list 'node field-name …))]
+         (list 'incomplete 'node field-name …))]
 
+Since the incomplete type for fields will appear in two different places, above
+and in the incomplete-to-with-promises conversion routine below, we write it in
+a separate chunk:
+
+@chunk[<field/incomplete-type>
+       (tmpl-replace-in-type field-type
+                             [node (U node/incomplete-type
+                                      node/compatible-placeholder-types …)]
+                             …)]
+
+We must however compute for each node the set of compatible placeholder types.
+We do that
+
+@chunk[<define-compatible-placeholder-types>
+       (define/with-syntax ((node/compatible-placeholder-types ...) ...)
+         (for/list ([x (in-syntax #'(node ...))])
+           (multiassoc-syntax
+            x
+            #'([result-type . (List 'placeholder 'mapping param-type ...)]
+               …))))]
+
+The multiassoc-syntax function used above filters the associative syntax list
+and returns the @tc[stx-cdr] of the matching elements, therefore returning a
+list of @tc[mapping/placeholder-type]s for which the @tc[result-type] is the
+given @tc[node] name.
+
+@chunk[<multiassoc-syntax>
+       (define (multiassoc-syntax query alist)
+         (map stx-cdr
+              (filter (λ (xy) (free-identifier=? query (stx-car xy)))
+                      (syntax->list alist))))
+       
+       (define (cdr-assoc-syntax query alist)
+         (stx-cdr (findf (λ (xy) (free-identifier=? query (stx-car xy)))
+                         (syntax->list alist))))
+       
+       (define-template-metafunction (tmpl-cdr-assoc-syntax stx)
+         (syntax-parse stx
+           [(_ query [k . v] …)
+            (cdr-assoc-syntax #'query #'([k . v] …))]))]
+
+The code above also needs some identifiers derived from @tc[node] and
+@tc[field-name]s:
+
+@; TODO: format-ids doesn't accept arbitrary values. Should we change it?
 @chunk[<define-ids>
        (define-temp-ids "~a/make-incomplete" (node …))
        (define-temp-ids "~a/incomplete-type" (node …))
-       ;; TODO: format-ids doesn't accept arbitrary values. Should we change it?
+       (define-temp-ids "~a/incomplete-fields" (node …))
        (define/with-syntax ((field/incomplete-type …) …)
-         (stx-map generate-temporaries #'((field-type …) …)))]
+         (stx-map generate-temporaries #'((field-name …) …)))]
+
+@subsection{Converting incomplete nodes to with-promises ones}
+
+@chunk[<convert-incomplete-to-with-promises>
+       [node/incomplete-type
+        node/with-promises-type
+        (λ (x) (and (pair? x)
+                    (eq? (car x) 'incomplete)
+                    (pair? (cdr x))
+                    (eq? (cadr x) 'node)))
+        (λ ([x : node/incomplete-type] [acc : Void])
+          (if (eq? (car x) 'incomplete)
+              <convert-incomplete-successor>
+              <convert-placeholder-successor>))]]
+
+@chunk[<convert-incomplete-successor>
+       (error (~a "Not implemented yet " x))]
+
+@chunk[<convert-placeholder-successor>
+       (% tag new-Δ-queues = (get-tag (cadr x) x Δ-queues)
+          (error (~a "Not implemented yet " x)))]
+
 
 @subsection{Processing the placeholders}
 
-@chunk[<fold-queue-body>
+@; TODO: also allow returning a placeholder (which means we should then
+@; process that placeholder in turn). The placeholder should return the
+@; same node type, but can use a different mapping?
+@; Or maybe we can do this from the ouside, using a wrapper macro?
+
+@CHUNK[<fold-queue-body>
+       (let ([mapping-result (apply mapping/function (cddr e))])
+         (tmpl-fold-instance (tmpl-cdr-assoc-syntax
+                              result-type
+                              [node . (List 'incomplete
+                                            'node
+                                            <field/incomplete-type> …)]
+                              …)
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             Void
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+                             <convert-incomplete-to-with-promises> …))
        'todo!]
 
+@section{The mapping functions}
+
+We define the mapping functions as they are described by the user, with an
+important change: Instead of returning an @emph{ideal} node type, we expect them
+to return an incomplete node type.
+
+@chunk[<define-mapping-function>
+       (define-type mapping/incomplete-result-type
+         (tmpl-replace-in-type result-type
+                               [node node/incomplete-type]
+                               …))
+       
+       (: mapping/function (→ param-type … mapping/incomplete-result-type))
+       (define mapping/function
+         (let ([mapping mapping/make-placeholder]
+               …
+               [node node/make-incomplete]
+               …)
+           (λ (param …)
+             . mapping-body)))]
+
+@chunk[<define-ids>
+       (define-temp-ids "~a/function" (mapping ...))
+       (define-temp-ids "~a/incomplete-result-type" (mapping ...))]
 
 @section{Temporary fillers}
 
@@ -361,12 +502,15 @@ which return type is the desired node type.
 @chunk[<make-graph-constructor>
        (define-syntax/parse <signature>
          <define-ids>
-         (template
-          (let ()
-            (begin <define-placeholder>) ...
-            (begin <define-with-promises>) ...
-            (begin <define-incomplete>) ...
-            <fold-queue>)))]
+         <define-compatible-placeholder-types>
+         ((λ (x) (pretty-write (syntax->datum x)) x)
+          (template
+           (let ()
+             (begin <define-mapping-placeholder>) …
+             (begin <define-with-promises-nodes>) …
+             (begin <define-incomplete-nodes>) …
+             (begin <define-mapping-function>) …
+             <fold-queue>))))]
 
 @section{Conclusion}
 
@@ -376,13 +520,18 @@ which return type is the desired node type.
                               racket/syntax
                               syntax/stx
                               syntax/parse/experimental/template
+                              racket/sequence
+                              racket/pretty; DEBUG
+                              alexis/util/threading; DEBUG
                               "rewrite-type.lp2.rkt"
                               "../lib/low-untyped.rkt")
+                  alexis/util/threading; DEBUG
                   "fold-queues.lp2.rkt"
                   "rewrite-type.lp2.rkt"
                   "../lib/low.rkt")
          
-         (provide fold-queues)
+         (begin-for-syntax
+           <multiassoc-syntax>)
          
          (provide make-graph-constructor)
          <make-graph-constructor>)]
@@ -390,12 +539,43 @@ which return type is the desired node type.
 @chunk[<module-test>
        (module* test typed/racket
          (require (submod "..")
+                  "fold-queues.lp2.rkt"; DEBUG
+                  "rewrite-type.lp2.rkt"; DEBUG
+                  "../lib/low.rkt"; DEBUG
                   typed/rackunit)
          
          <use-example>
          
          g
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
          
+
          (require (submod ".." doc)))]
 
 @chunk[<*>
diff --git a/graph/graph/rewrite-type.lp2.rkt b/graph/graph/rewrite-type.lp2.rkt
index 1f92c2f..610061e 100644
--- a/graph/graph/rewrite-type.lp2.rkt
+++ b/graph/graph/rewrite-type.lp2.rkt
@@ -15,7 +15,7 @@ For example, one could replace all strings in a data structure by their length:
 @CHUNK[<test-example>
        (make-replace test-example
                      (Vectorof (U (List 'tag1 String) (List 'tag2 Number)))
-                     [String Number string-length])]
+                     [String Number string? string-length])]
 
 The result's type would be derived from the original one, but all occurrences of
 @tc[String] have been replaced by @tc[Number]. The result itself would have the
@@ -35,13 +35,13 @@ relies on the lower-level utilities provided by this module, namely
 @CHUNK[<test-make-replace>
        (define-syntax (make-replace stx)
          (syntax-case stx ()
-           [(_ name type [from to fun] ...)
+           [(_ name type [from to pred? fun] ...)
             #`(begin
                 (: name (→ type #,(replace-in-type #'type #'([from to] ...))))
                 (define (name v)
                   #,(replace-in-instance #'v
                                          #'type
-                                         #'([from to fun] ...))))]))]
+                                         #'([from to pred? fun] ...))))]))]
 
 @subsection{A bigger example}
 
@@ -58,7 +58,7 @@ example:
                                                         Number
                                                         (Listof String))))
                                    String))
-                     [String Number string-length])]
+                     [String Number string? string-length])]
 
 The replacement function @tc[test-big] defined above will, as expected, have a
 return type containing no more strings, and the correct return value.
@@ -268,9 +268,9 @@ functions is undefined.
        (make-fold test-fold-1
                   (List String Number (List String String Symbol String))
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal? (test-fold-1 '("a" 7 ("bb" "cccc" x "dddddddd")) 0)
                      '((1 7 (2 4 x 8)) . 15))]
@@ -279,9 +279,9 @@ functions is undefined.
        (make-fold test-fold-list
                   (List String Number (Pairof String String) Symbol)
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal? (test-fold-list '("a" 9 ("bb" . "cccc") x) 0)
                      '((1 9 (2 . 4) x) . 7))]
@@ -290,9 +290,9 @@ functions is undefined.
        (make-fold test-fold-pairof
                   (Pairof String (Pairof Number String))
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal? (test-fold-pairof '("a" 7 . "bb") 0)
                      '((1 7 . 2) . 3))]
@@ -301,9 +301,9 @@ functions is undefined.
        (make-fold test-fold-listof
                   (List String Number (Listof String) Symbol String)
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal? (test-fold-listof
                       '("a" 7 ("bb" "cccc" "dddddddd") x "eeeeeeeeeeeeeeee")
@@ -314,9 +314,9 @@ functions is undefined.
        (make-fold test-fold-vector
                   (Vector String Number (Vectorof String) Symbol String)
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal? (test-fold-vector
                       '#("a" 7 #("bb" "cccc" "dddddddd") x "eeeeeeeeeeeeeeee")
@@ -327,9 +327,9 @@ functions is undefined.
        (make-fold test-fold-vectorof
                   (Vectorof (U (List 'tag1 String String) (List 'tag2 Number)))
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal? (test-fold-vectorof
                       '#((tag1 "a" "bb") (tag2 7) (tag1 "cccc" "dddddddd"))
@@ -347,9 +347,9 @@ functions is undefined.
                                                      (Listof String))))
                                 String))
                   Number
-                  [String Number (λ ([x : String] [acc : Number])
-                                   (values (string-length x)
-                                           (+ acc (string-length x))))])
+                  [String Number string? (λ ([x : String] [acc : Number])
+                                           (values (string-length x)
+                                                   (+ acc (string-length x))))])
        
        (check-equal?
         (test-fold-big '(((tag2 (#(sym) 7 ("a" "bb" "cccc"))) . "dddddddd")) 0)
@@ -358,7 +358,7 @@ functions is undefined.
 @CHUNK[<test-make-fold>
        (define-syntax (make-fold stx)
          (syntax-case stx ()
-           [(_ name type acc-type [from to fun] ...)
+           [(_ name type acc-type [from to pred? fun] ...)
             #`(begin
                 (: name (→ type
                            acc-type
@@ -370,7 +370,7 @@ functions is undefined.
                                  [res-acc : acc-type])
                                 (#,(fold-instance #'type
                                                   #'acc-type
-                                                  #'([from to fun] ...))
+                                                  #'([from to pred? fun] ...))
                                  val
                                  acc)])
                     (cons res res-acc))))]))]
@@ -380,7 +380,7 @@ functions is undefined.
 @CHUNK[<fold-instance>
        (define-for-syntax (fold-instance t stx-acc-type r)
          (define/with-syntax acc-type stx-acc-type)
-         (define/with-syntax ([from to fun] ...) r)
+         (define/with-syntax ([from to pred? fun] ...) r)
          <recursive-replace-fold-instance>
          (recursive-replace t))]
 
@@ -491,21 +491,37 @@ functions is undefined.
            [x:id
             #'(inst values x acc-type)]))]
 
+@subsection{Union types}
+
 @CHUNK[<replace-fold-union>
        (syntax-parse ta
          [(List ((~literal quote) tag:id) b ...)
-          <replace-fold-tagged-union-instance>]
+          <replace-fold-union-tagged-list>]
+         [(Pairof ((~literal quote) tag:id) b)
+          <replace-fold-union-tagged-list>]
+         [x:id
+          #:attr assoc-result (stx-assoc #'x #'((from to pred? fun) ...))
+          #:when (attribute assoc-result)
+          #:with (x-from x-to x-pred? x-fun) #'assoc-result
+          <replace-fold-union-predicate>]
          [_ (error "Type-replace on untagged Unions isn't supported yet!")])]
 
 For cases of the union which are a tagged list, we use a simple guard, and call
 @tc[recursive-replace] on the whole @tc[(List 'tag b ...)] type.
 
-@CHUNK[<replace-fold-tagged-union-instance>
-       #`[(and (list? val)
-               (not (null? val))
+@CHUNK[<replace-fold-union-tagged-list>
+       #`[(and (pair? val)
                (eq? 'tag (car val)))
           (#,(recursive-replace ta) val acc)]]
 
+For cases of the union which match one of the types to be replaced, we use the
+provided predicate as a guard, and call @tc[recursive-replace] on the whole
+type.
+
+@CHUNK[<replace-fold-union-predicate>
+       #`[(x-pred? val)
+          (#,(recursive-replace ta) val acc)]]
+
 @section{Replacing parts of an instance using fold}
 
 We can use the @tc[fold-instance] for-syntax function defined in section
@@ -518,12 +534,12 @@ implementation.
 
 @CHUNK[<replace-in-instance2>
        (define-for-syntax (replace-in-instance2 val t r)
-         (define/with-syntax ([from to fun] ...) r)
+         (define/with-syntax ([from to pred? fun] ...) r)
          #`(first-value
             (#,(fold-instance t
                               #'Void
-                              #'([from to (λ ([x : from] [acc : Void])
-                                            (values (fun x) acc))]
+                              #'([from to pred? (λ ([x : from] [acc : Void])
+                                                  (values (fun x) acc))]
                                  ...))
              #,val
              (void))))]
@@ -548,11 +564,13 @@ And one each for @tc[fold-instance] and @tc[replace-in-instance2]:
 @CHUNK[<template-metafunctions>
        (define-template-metafunction (tmpl-fold-instance stx)
          (syntax-parse stx
-           [(_ type:expr acc-type:expr [from to fun] …)
+           [(_ type:expr acc-type:expr [from to pred? fun] …)
             #`(begin
                 "fold-instance expanded code below. Initially called with:"
-                '(fold-instance type acc-type [from to fun] …)
-                #,(fold-instance #'type #'acc-type #'([from to fun] …)))]))
+                '(fold-instance type acc-type [from to pred? fun] …)
+                #,(fold-instance #'type
+                                 #'acc-type
+                                 #'([from to pred? fun] …)))]))
        
        (define-template-metafunction (tmpl-replace-in-instance stx)
          (syntax-parse stx
diff --git a/graph/lib/low.rkt b/graph/lib/low.rkt
index 37f5924..e495fd6 100644
--- a/graph/lib/low.rkt
+++ b/graph/lib/low.rkt
@@ -714,6 +714,8 @@
 
 ;; ==== type-inference-helpers.rkt ====
 
+(provide cars cdrs)
+
 #|
 ;; This does not work, in the end.
 (provide imap)
@@ -729,6 +731,12 @@
          (inlined-map lst))]))
 |#
 
+(: cars (∀ (A) (→ (Listof (Pairof A Any)) (Listof A))))
+(define (cars l) ((inst map A (Pairof A Any)) car l))
+
+(: cdrs (∀ (B) (→ (Listof (Pairof Any B)) (Listof B))))
+(define (cdrs l) ((inst map B (Pairof Any B)) cdr l))
+
 ;; ==== percent.rkt ====
 
 (provide % define%)