diff --git a/Makefile b/Makefile
index 5ae8065..1ed800b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,17 @@
+LITERATE_MD=unquoting.md
+
+all: $(LITERATE_MD) preserves.pdf
+
 preserves.pdf: preserves.md preserves.css
 	google-chrome --headless --disable-gpu --print-to-pdf=$@ \
 		http://localhost:4000/preserves/preserves.html
 
+clean:
+	rm -f $(LITERATE_MD)
+
+%.md: %.rkt
+	literate-lisp-to-markdown < $< > $@
+
 test-all:
 	make -C tests
 	(cd implementations/javascript; npm test)
diff --git a/unquoting.md b/unquoting.md
new file mode 100644
index 0000000..0c7d588
--- /dev/null
+++ b/unquoting.md
@@ -0,0 +1,394 @@
+---
+title: (Un)quotation in layered pub/sub networks
+---
+<!--
+```racket
+#lang racket
+(require rackunit)
+(require racket/contract)
+```
+-->
+
+Tony Garnock-Jones <tonyg@leastfixedpoint.com>  
+June 2020.
+
+## Introduction
+
+There's potential for confusion whenever *patterns* are drawn from
+the same set that the *values to be matched* come from.
+
+In layered pub/sub networks like
+[Syndicate](https://syndicate-lang.org/), publisher-subscriber
+relationships are set up using messages carried over the
+publish-subscribe medium itself.
+
+Subscribers build messages containing patterns describing other
+messages they are interested in.
+
+But in general, these messages travel across multiple layered
+pub/sub dataspaces. To avoid confusion, we have to be very clear
+about when a piece of data denotes a pattern and when it is just a
+piece of data.
+
+In this post, I'll describe the approach I want to take to solve
+this problem for Syndicate in the general case.
+
+### What's the problem?
+
+Consider regular expressions. The regex `ab*c` matches `ac`,
+`abc`, `abbc`, and so on; but what if we wanted to match the
+literal string `ab*c`? We have to escape the star in the pattern,
+writing the pattern as `ab\*c`.
+
+#### Quotation
+
+If we want to use a regex engine to search for a literal string
+supplied by someone else---perhaps a user, perhaps an API
+client---we have to take care to *quote* the literal string, in
+order to avoid confusion caused by metacharacters:[^racket-regexp-quote]
+
+| Literal string        | Quoted form                  |
+| ---                   | ---                          |
+| `no metachars`        | `no metachars`               |
+| `ab*c`                | `ab\*c`                      |
+| `...`                 | `\.\.\.`                     |
+| `(hello \$\ [world])` | `\(hello \\\$\\ \[world\]\)` |
+
+[^racket-regexp-quote]: Racket supplies
+    [`regexp-quote`](https://github.com/racket/racket/blob/5bb837661c12a9752c6a99f952c0e1b267645b33/racket/collects/racket/private/string.rkt#L38-L51)
+    ([docs](https://docs.racket-lang.org/reference/regexp.html?q=reg%20quo#(def._((lib._racket%2Fprivate%2Fbase..rkt)._regexp-quote))))
+    for this purpose:
+```racket
+(check-equal? (regexp-quote "ab*c")                  "ab\\*c")
+(check-equal? (regexp-quote "...")                   "\\.\\.\\.")
+(check-equal? (regexp-quote "(hello \\$\\ [world])") "\\(hello \\\\\\$\\\\ \\[world\\]\\)")
+```
+
+#### Invariant
+
+The invariant we want to rely on is
+
+> every string, after quotation, becomes a regular expression that matches
+> exactly and only the original string.[^racket-regexp-quotation-invariant]
+
+[^racket-regexp-quotation-invariant]:
+    Expressing this in code is straightforward:
+```racket
+(define (regexp-quotation-invariant original-string some-other-string)
+  (equal? (string=? original-string some-other-string)
+          (regexp-match? (regexp-quote original-string) some-other-string)))
+```
+    We could use Racket's [random data
+    generation](https://docs.racket-lang.org/data/Enumerations.html?q=data%2Fen#%28mod-path._data%2Fenumerate%29)
+    tools to perform randomized testing of this invariant.
+
+Of course, this same problem crops up in any pattern language
+where embedding of values in patterns makes sense, so let's
+generalize accordingly:
+
+> every value, after quotation, becomes a pattern that matches
+> exactly and only the original value.
+
+
+### Quotation of pub/sub patterns.
+
+In [Syndicate](https://syndicate-lang.org/), we want patterns over
+assertions (and thus over messages) to be able to match arbitrary
+[Preserves](.) atoms, sequences, and records.
+
+However, to date, there have been special exceptions. The special
+records `capture/1` and `discard/0`, embedded in patterns, have
+been interpreted as defining pattern variables and wildcards,
+respectively. There has been no way to construct a pattern that
+matches `capture/1` or `discard/0` records themselves.
+
+Previously, I tried adding a `quote/1` record to the set of
+special record types. Experimentation [demonstrated](quoting.rkt)
+that patterns with `quote/1` were able to escape the limitations
+of patterns without `quote/1`. Also, it's [a theorem](quoting.v)
+that quoting is "sensible": that unquotation after quotation of a
+pattern always equals the original pattern.
+
+In this post, I'll explore an alternative I think might be better:
+letting patterns match anything except a *single* special record,
+`unquote/1`. Patterns use `unquote/1` to escape into a
+*metalanguage* where special operators like capture, discard, and
+so on can be discussed.
+
+## Definitions
+
+We'll work with a simplified data language. Instead of full
+Preserves, which includes lists, maps, records, a variety of atoms
+and so forth, we'll stick to just records and atoms.
+
+`Value`s are the things our `Pattern`s are to match.
+
+`Value`s that are `Lists` denote records: the first `Value` is the
+label of the record, and the remaining `Value`s are its fields.
+
+```racket
+(define (record? x)
+  (and (list? x)
+       (positive? (length x))
+       (andmap value? x)))
+
+(define (record-label x) (car x))
+(define (record-fields x) (cdr x))
+(define (record-arity x) (length (record-fields x)))
+(define (record-field x n) (list-ref x (+ n 1)))
+```
+
+Atoms, then, are the non-`List` `Value`s.
+
+```racket
+(define (atom? x)
+  (or (string? x)
+      (symbol? x)
+      (number? x)))
+```
+
+`Value`s are the records and the atoms, and nothing else.
+
+```racket
+(define (value? x)
+  (or (atom? x)
+      (record? x)))
+```
+
+We will frequently need to decide whether a `Value` is a record
+with a particular label and arity.
+
+```racket
+(define (record/class? x label arity)
+  (and (record? x)
+       (equal? (record-label x) label)
+       (= (record-arity x) arity)))
+```
+
+A `Pattern` is a `Value` with certain additional constraints on
+the `Operation`s that appear within an `unquote/1` record.
+
+```racket
+(define (pattern? x)
+  (and (value? x)
+       (or (atom? x)
+           (if (record/class? x 'unquote 1)
+               (operation? (record-field x 0))
+               (andmap pattern? x)))))
+```
+
+A valid `Operation` is either a `capture/1`, containing another
+pattern; a `discard/0`, denoting wildcard; or `quote/1`, which
+promotes an *arbitrary* `Value` to a literal-matching `Pattern`.
+This last one is what allows us to write patterns that match
+`unquote/1` values without tripping over ourselves.
+
+```racket
+(define (operation? x)
+  (cond [(record/class? x 'capture 1) (pattern? (record-field x 0))]
+        [(record/class? x 'discard 0) #t]
+        [(record/class? x 'quote 1) (value? (record-field x 0))]
+        [else #f]))
+```
+
+**Examples**.
+
+```racket
+(check-true (pattern? 123))
+(check-true (pattern? "Hello"))
+(check-true (pattern? 'capture))
+(check-true (pattern? 'unquote))
+(check-true (pattern? '(Present "Tony")))
+(check-true (pattern? '(Says "Tony" "Hello, world!")))
+(check-true (pattern? '(Says "Tony" (capture (discard)))))
+(check-true (pattern? '(Says "Tony" (unquote (capture (discard))))))
+```
+
+Since `pattern?` subsumes `value?`, we see that each of these is
+both a `Value` and a `Pattern`. However, the following term is a
+`Value` but not a `Pattern`, because it does not conform to the
+definition of the `unquote`d `Operation`s.
+
+<!--
+```racket
+(let ()
+```
+-->
+```racket
+(define non-pattern '(Says "Tony" (unquote (noise))))
+(check-true (value? non-pattern))
+(check-false (pattern? non-pattern))
+```
+<!--
+```racket
+)
+```
+-->
+
+We may use `quote` in conjunction with `unquote` to specify a
+pattern that will match our `non-pattern` example:
+
+```racket
+(check-true (pattern? '(Says "Tony" ((unquote (quote unquote)) (noise)))))
+```
+
+We may also abuse the Lisp notation for quotation and
+quasiquotation when writing such patterns, which helps make them a
+little shorter and perhaps easier to read:
+
+```racket
+(check-true (pattern? '(Says "Tony" (,'unquote (noise)))))
+```
+
+Finally, this term isn't even a `Value`: it includes an empty list
+within it.
+
+```racket
+(check-false (value? '(Says "Tony" ())))
+```
+
+## Pattern matching
+
+Let's call our matching operator `Match`, with a capital `M` to
+distinguish it from Racket's own `match` syntax.
+
+`Match`, given a `pat`tern and a `val`ue, should answer either a
+`List` of the captured values in depth-first, left-to-right order,
+if the pattern matches the value, or `#f` if the arguments do not
+match.
+
+```racket
+;; ;; Precondition: (and (pattern? pat) (value? val))
+;; (define (Match pat val)
+
+;; ;;; First of all, let's take care of matching atoms.
+
+;;   (cond [(atom? pat) (if (equal? pat val) '() #f)]
+
+;; ;;; Next, the special pattern record `unquote/1` and the operators it
+;; ;;; contains.
+
+;;         [(record/class? pat 'unquote 1)
+;;          (define op (record-field pat 0))
+
+;; ;;; A `capture/1` should prepend the current `val`ue to a succeeding
+;; ;;; submatch, and should propagate a failing submatch.
+
+;;          (cond [(record/class? op 'capture 1)
+;;                 (define r (Match (record-field op 0) val))
+;;                 (and r (cons val r))]
+
+;; ;;; A `discard/0` should accept any `val`ue, yielding a success result
+;; ;;; containing no captures.
+
+;;                [(record/class? op 'discard 0)
+;;                 '()]
+
+;; ;;; Finally, a `quote/1` should match exactly its argument and nothing
+;; ;;; else.
+
+;;                [(record/class? op 'quote 1)
+;;                 (if (equal? (record-field op 0) val) '() #f)]
+```
+
+---------------------------------------------------------------------------
+
+```racket
+;; (struct DISCARD ())
+;; (struct CAPTURE (p))
+
+;; (define (q p)
+;;   (match p
+;;     [(DISCARD) `(discard)]
+;;     [(CAPTURE p) `(capture ,(q p))]
+;;     [`(discard) `('discard)]
+;;     [`(capture ,p) `('capture ,(q p))]
+;;     [`(quote ,p) `('quote ,(q p))]
+;;     [`(,pa . ,pd) `(,(q pa) . ,(q pd))]
+;;     [a a]))
+
+;; (define (uq p)
+;;   (match p
+;;     [`(discard) (DISCARD)]
+;;     [`(capture ,p) (CAPTURE (uq p))]
+;;     [`(quote ,p) p]
+;;     [`(,pa . ,pd) `(,(uq pa) . ,(uq pd))]
+;;     [a a]))
+
+;; ;; Goal: (uq (q p)) === p
+
+;; ;; (define (m p v k)
+;; ;;   (match* (p v)
+;; ;;     [(`(discard) _) (k '())]
+;; ;;     [(`(capture ,p) v) (m p v (lambda (bs) (cons v bs)))]
+;; ;;     [(`(quote ,p) v) (and (equal? p v) (k '()))]
+;; ;;     [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
+;; ;;     [(p v) (and (equal? p v) (k '()))]))
+
+;; (define (m p v k)
+;;   (match* (p v)
+;;     [((DISCARD) _) (k '())]
+;;     [((CAPTURE p) v) (m p v (lambda (bs) (cons v bs)))]
+;;     [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
+;;     [(p v) (and (equal? p v) (k '()))]))
+
+;; (module+ test
+;;   (require rackunit)
+;;   ;; (define (M p v) (m p v values))
+;;   (define (M p v) (m (uq p) v values))
+;;   (check-equal? (M `(capture 1) 1) '(1))
+;;   (check-equal? (M `(discard) 1) '())
+;;   (check-equal? (M 1 1) '())
+;;   (check-equal? (M 2 1) #f)
+;;   (check-equal? (M `(capture 2) 1) #f)
+
+;;   (check-equal? (M `(record (capture (discard))) `(record value)) '(value))
+;;   (check-equal? (M `(record (capture (discard))) `(record 'value)) '('value))
+;;   (check-equal? (M `(record (capture (discard))) `(record (capture (discard))))
+;;                 '((capture (discard))))
+
+;;   (check-equal? (M `(record ('capture (discard))) `(record (capture (discard))))
+;;                 '())
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record (capture (discard))))
+;;                 '((capture (discard))))
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record 'value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record ('capture (discard))))
+;;                 #f)
+
+;;   (check-equal? (M `(record '(capture (discard))) `(record (capture (discard))))
+;;                 '())
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record (capture (discard))))
+;;                 '((capture (discard))))
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record 'value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record '(capture (discard))))
+;;                 #f)
+
+;;   (check-equal? (M `(record ('quote value)) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ('quote value))) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ('quote value))) `(record value)) #f)
+;;   (check-equal? (M `(record (capture ('quote value))) `(record 'value)) '('value))
+;;   (check-equal? (M `(record (capture ('quote value))) `(record 'notvalue)) #f)
+;;   (check-equal? (M `(record ('quote value)) `(record 'value)) '())
+;;   (check-equal? (M `(record (capture ('quote value))) `(record ('quote value))) #f)
+
+;;   (check-equal? (M `(record ''value) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ''value)) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ''value)) `(record value)) #f)
+;;   (check-equal? (M `(record (capture ''value)) `(record 'value)) '('value))
+;;   (check-equal? (M `(record (capture ''value)) `(record 'notvalue)) #f)
+;;   (check-equal? (M `(record ''value) `(record 'value)) '())
+;;   (check-equal? (M `(record (capture ''value)) `(record ''value)) #f)
+
+;;   (check-equal? (q (CAPTURE 1)) `(capture 1))
+;;   (check-equal? (q (DISCARD)) `(discard))
+;;   (check-equal? (q `(capture 1)) `('capture 1))
+;;   (check-equal? (q `(discard)) `('discard))
+
+;;   )
+```
diff --git a/unquoting.rkt b/unquoting.rkt
new file mode 100644
index 0000000..72ebed2
--- /dev/null
+++ b/unquoting.rkt
@@ -0,0 +1,358 @@
+;;; ---
+;;; title: (Un)quotation in layered pub/sub networks
+;;; ---
+;;; <!--
+#lang racket
+(require rackunit)
+(require racket/contract)
+;;; -->
+
+;;; Tony Garnock-Jones <tonyg@leastfixedpoint.com>  
+;;; June 2020.
+
+;;; ## Introduction
+
+;;; There's potential for confusion whenever *patterns* are drawn from
+;;; the same set that the *values to be matched* come from.
+
+;;; In layered pub/sub networks like
+;;; [Syndicate](https://syndicate-lang.org/), publisher-subscriber
+;;; relationships are set up using messages carried over the
+;;; publish-subscribe medium itself.
+
+;;; Subscribers build messages containing patterns describing other
+;;; messages they are interested in.
+
+;;; But in general, these messages travel across multiple layered
+;;; pub/sub dataspaces. To avoid confusion, we have to be very clear
+;;; about when a piece of data denotes a pattern and when it is just a
+;;; piece of data.
+
+;;; In this post, I'll describe the approach I want to take to solve
+;;; this problem for Syndicate in the general case.
+
+;;; ### What's the problem?
+
+;;; Consider regular expressions. The regex `ab*c` matches `ac`,
+;;; `abc`, `abbc`, and so on; but what if we wanted to match the
+;;; literal string `ab*c`? We have to escape the star in the pattern,
+;;; writing the pattern as `ab\*c`.
+
+;;; #### Quotation
+
+;;; If we want to use a regex engine to search for a literal string
+;;; supplied by someone else---perhaps a user, perhaps an API
+;;; client---we have to take care to *quote* the literal string, in
+;;; order to avoid confusion caused by metacharacters:[^racket-regexp-quote]
+
+;;; | Literal string        | Quoted form                  |
+;;; | ---                   | ---                          |
+;;; | `no metachars`        | `no metachars`               |
+;;; | `ab*c`                | `ab\*c`                      |
+;;; | `...`                 | `\.\.\.`                     |
+;;; | `(hello \$\ [world])` | `\(hello \\\$\\ \[world\]\)` |
+
+;;; [^racket-regexp-quote]: Racket supplies
+;;;     [`regexp-quote`](https://github.com/racket/racket/blob/5bb837661c12a9752c6a99f952c0e1b267645b33/racket/collects/racket/private/string.rkt#L38-L51)
+;;;     ([docs](https://docs.racket-lang.org/reference/regexp.html?q=reg%20quo#(def._((lib._racket%2Fprivate%2Fbase..rkt)._regexp-quote))))
+;;;     for this purpose:
+(check-equal? (regexp-quote "ab*c")                  "ab\\*c")
+(check-equal? (regexp-quote "...")                   "\\.\\.\\.")
+(check-equal? (regexp-quote "(hello \\$\\ [world])") "\\(hello \\\\\\$\\\\ \\[world\\]\\)")
+
+;;; #### Invariant
+
+;;; The invariant we want to rely on is
+;;;
+;;; > every string, after quotation, becomes a regular expression that matches
+;;; > exactly and only the original string.[^racket-regexp-quotation-invariant]
+
+;;; [^racket-regexp-quotation-invariant]:
+;;;     Expressing this in code is straightforward:
+(define (regexp-quotation-invariant original-string some-other-string)
+  (equal? (string=? original-string some-other-string)
+          (regexp-match? (regexp-quote original-string) some-other-string)))
+;;;     We could use Racket's [random data
+;;;     generation](https://docs.racket-lang.org/data/Enumerations.html?q=data%2Fen#%28mod-path._data%2Fenumerate%29)
+;;;     tools to perform randomized testing of this invariant.
+
+;;; Of course, this same problem crops up in any pattern language
+;;; where embedding of values in patterns makes sense, so let's
+;;; generalize accordingly:
+;;;
+;;; > every value, after quotation, becomes a pattern that matches
+;;; > exactly and only the original value.
+
+
+;;; ### Quotation of pub/sub patterns.
+
+;;; In [Syndicate](https://syndicate-lang.org/), we want patterns over
+;;; assertions (and thus over messages) to be able to match arbitrary
+;;; [Preserves](.) atoms, sequences, and records.
+
+;;; However, to date, there have been special exceptions. The special
+;;; records `capture/1` and `discard/0`, embedded in patterns, have
+;;; been interpreted as defining pattern variables and wildcards,
+;;; respectively. There has been no way to construct a pattern that
+;;; matches `capture/1` or `discard/0` records themselves.
+
+;;; Previously, I tried adding a `quote/1` record to the set of
+;;; special record types. Experimentation [demonstrated](quoting.rkt)
+;;; that patterns with `quote/1` were able to escape the limitations
+;;; of patterns without `quote/1`. Also, it's [a theorem](quoting.v)
+;;; that quoting is "sensible": that unquotation after quotation of a
+;;; pattern always equals the original pattern.
+;;;
+;;; In this post, I'll explore an alternative I think might be better:
+;;; letting patterns match anything except a *single* special record,
+;;; `unquote/1`. Patterns use `unquote/1` to escape into a
+;;; *metalanguage* where special operators like capture, discard, and
+;;; so on can be discussed.
+
+;;; ## Definitions
+;;;
+;;; We'll work with a simplified data language. Instead of full
+;;; Preserves, which includes lists, maps, records, a variety of atoms
+;;; and so forth, we'll stick to just records and atoms.
+;;;
+;;; `Value`s are the things our `Pattern`s are to match.
+;;;
+;;; `Value`s that are `Lists` denote records: the first `Value` is the
+;;; label of the record, and the remaining `Value`s are its fields.
+
+(define (record? x)
+  (and (list? x)
+       (positive? (length x))
+       (andmap value? x)))
+
+(define (record-label x) (car x))
+(define (record-fields x) (cdr x))
+(define (record-arity x) (length (record-fields x)))
+(define (record-field x n) (list-ref x (+ n 1)))
+
+;;; Atoms, then, are the non-`List` `Value`s.
+
+(define (atom? x)
+  (or (string? x)
+      (symbol? x)
+      (number? x)))
+
+;;; `Value`s are the records and the atoms, and nothing else.
+
+(define (value? x)
+  (or (atom? x)
+      (record? x)))
+
+;;; We will frequently need to decide whether a `Value` is a record
+;;; with a particular label and arity.
+
+(define (record/class? x label arity)
+  (and (record? x)
+       (equal? (record-label x) label)
+       (= (record-arity x) arity)))
+
+;;; A `Pattern` is a `Value` with certain additional constraints on
+;;; the `Operation`s that appear within an `unquote/1` record.
+
+(define (pattern? x)
+  (and (value? x)
+       (or (atom? x)
+           (if (record/class? x 'unquote 1)
+               (operation? (record-field x 0))
+               (andmap pattern? x)))))
+
+;;; A valid `Operation` is either a `capture/1`, containing another
+;;; pattern; a `discard/0`, denoting wildcard; or `quote/1`, which
+;;; promotes an *arbitrary* `Value` to a literal-matching `Pattern`.
+;;; This last one is what allows us to write patterns that match
+;;; `unquote/1` values without tripping over ourselves.
+
+(define (operation? x)
+  (cond [(record/class? x 'capture 1) (pattern? (record-field x 0))]
+        [(record/class? x 'discard 0) #t]
+        [(record/class? x 'quote 1) (value? (record-field x 0))]
+        [else #f]))
+
+;;; **Examples**.
+
+(check-true (pattern? 123))
+(check-true (pattern? "Hello"))
+(check-true (pattern? 'capture))
+(check-true (pattern? 'unquote))
+(check-true (pattern? '(Present "Tony")))
+(check-true (pattern? '(Says "Tony" "Hello, world!")))
+(check-true (pattern? '(Says "Tony" (capture (discard)))))
+(check-true (pattern? '(Says "Tony" (unquote (capture (discard))))))
+
+;;; Since `pattern?` subsumes `value?`, we see that each of these is
+;;; both a `Value` and a `Pattern`. However, the following term is a
+;;; `Value` but not a `Pattern`, because it does not conform to the
+;;; definition of the `unquote`d `Operation`s.
+
+;;; <!--
+(let ()
+;;; -->
+(define non-pattern '(Says "Tony" (unquote (noise))))
+(check-true (value? non-pattern))
+(check-false (pattern? non-pattern))
+;;; <!--
+)
+;;; -->
+
+;;; We may use `quote` in conjunction with `unquote` to specify a
+;;; pattern that will match our `non-pattern` example:
+
+(check-true (pattern? '(Says "Tony" ((unquote (quote unquote)) (noise)))))
+
+;;; We may also abuse the Lisp notation for quotation and
+;;; quasiquotation when writing such patterns, which helps make them a
+;;; little shorter and perhaps easier to read:
+
+(check-true (pattern? '(Says "Tony" (,'unquote (noise)))))
+
+;;; Finally, this term isn't even a `Value`: it includes an empty list
+;;; within it.
+
+(check-false (value? '(Says "Tony" ())))
+
+;;; ## Pattern matching
+;;;
+;;; Let's call our matching operator `Match`, with a capital `M` to
+;;; distinguish it from Racket's own `match` syntax.
+;;;
+;;; `Match`, given a `pat`tern and a `val`ue, should answer either a
+;;; `List` of the captured values in depth-first, left-to-right order,
+;;; if the pattern matches the value, or `#f` if the arguments do not
+;;; match.
+
+;; ;; Precondition: (and (pattern? pat) (value? val))
+;; (define (Match pat val)
+
+;; ;;; First of all, let's take care of matching atoms.
+
+;;   (cond [(atom? pat) (if (equal? pat val) '() #f)]
+
+;; ;;; Next, the special pattern record `unquote/1` and the operators it
+;; ;;; contains.
+
+;;         [(record/class? pat 'unquote 1)
+;;          (define op (record-field pat 0))
+
+;; ;;; A `capture/1` should prepend the current `val`ue to a succeeding
+;; ;;; submatch, and should propagate a failing submatch.
+
+;;          (cond [(record/class? op 'capture 1)
+;;                 (define r (Match (record-field op 0) val))
+;;                 (and r (cons val r))]
+
+;; ;;; A `discard/0` should accept any `val`ue, yielding a success result
+;; ;;; containing no captures.
+
+;;                [(record/class? op 'discard 0)
+;;                 '()]
+
+;; ;;; Finally, a `quote/1` should match exactly its argument and nothing
+;; ;;; else.
+
+;;                [(record/class? op 'quote 1)
+;;                 (if (equal? (record-field op 0) val) '() #f)]
+
+;;; ---------------------------------------------------------------------------
+
+;; (struct DISCARD ())
+;; (struct CAPTURE (p))
+
+;; (define (q p)
+;;   (match p
+;;     [(DISCARD) `(discard)]
+;;     [(CAPTURE p) `(capture ,(q p))]
+;;     [`(discard) `('discard)]
+;;     [`(capture ,p) `('capture ,(q p))]
+;;     [`(quote ,p) `('quote ,(q p))]
+;;     [`(,pa . ,pd) `(,(q pa) . ,(q pd))]
+;;     [a a]))
+
+;; (define (uq p)
+;;   (match p
+;;     [`(discard) (DISCARD)]
+;;     [`(capture ,p) (CAPTURE (uq p))]
+;;     [`(quote ,p) p]
+;;     [`(,pa . ,pd) `(,(uq pa) . ,(uq pd))]
+;;     [a a]))
+
+;; ;; Goal: (uq (q p)) === p
+
+;; ;; (define (m p v k)
+;; ;;   (match* (p v)
+;; ;;     [(`(discard) _) (k '())]
+;; ;;     [(`(capture ,p) v) (m p v (lambda (bs) (cons v bs)))]
+;; ;;     [(`(quote ,p) v) (and (equal? p v) (k '()))]
+;; ;;     [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
+;; ;;     [(p v) (and (equal? p v) (k '()))]))
+
+;; (define (m p v k)
+;;   (match* (p v)
+;;     [((DISCARD) _) (k '())]
+;;     [((CAPTURE p) v) (m p v (lambda (bs) (cons v bs)))]
+;;     [(`(,pa . ,pd) `(,va . ,vd)) (m pa va (lambda (bs) (m pd vd (lambda (cs) (k (append bs cs))))))]
+;;     [(p v) (and (equal? p v) (k '()))]))
+
+;; (module+ test
+;;   (require rackunit)
+;;   ;; (define (M p v) (m p v values))
+;;   (define (M p v) (m (uq p) v values))
+;;   (check-equal? (M `(capture 1) 1) '(1))
+;;   (check-equal? (M `(discard) 1) '())
+;;   (check-equal? (M 1 1) '())
+;;   (check-equal? (M 2 1) #f)
+;;   (check-equal? (M `(capture 2) 1) #f)
+
+;;   (check-equal? (M `(record (capture (discard))) `(record value)) '(value))
+;;   (check-equal? (M `(record (capture (discard))) `(record 'value)) '('value))
+;;   (check-equal? (M `(record (capture (discard))) `(record (capture (discard))))
+;;                 '((capture (discard))))
+
+;;   (check-equal? (M `(record ('capture (discard))) `(record (capture (discard))))
+;;                 '())
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record (capture (discard))))
+;;                 '((capture (discard))))
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record 'value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture ('capture (discard)))) `(record ('capture (discard))))
+;;                 #f)
+
+;;   (check-equal? (M `(record '(capture (discard))) `(record (capture (discard))))
+;;                 '())
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record (capture (discard))))
+;;                 '((capture (discard))))
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record 'value))
+;;                 #f)
+;;   (check-equal? (M `(record (capture '(capture (discard)))) `(record '(capture (discard))))
+;;                 #f)
+
+;;   (check-equal? (M `(record ('quote value)) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ('quote value))) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ('quote value))) `(record value)) #f)
+;;   (check-equal? (M `(record (capture ('quote value))) `(record 'value)) '('value))
+;;   (check-equal? (M `(record (capture ('quote value))) `(record 'notvalue)) #f)
+;;   (check-equal? (M `(record ('quote value)) `(record 'value)) '())
+;;   (check-equal? (M `(record (capture ('quote value))) `(record ('quote value))) #f)
+
+;;   (check-equal? (M `(record ''value) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ''value)) `(record (capture (discard)))) #f)
+;;   (check-equal? (M `(record (capture ''value)) `(record value)) #f)
+;;   (check-equal? (M `(record (capture ''value)) `(record 'value)) '('value))
+;;   (check-equal? (M `(record (capture ''value)) `(record 'notvalue)) #f)
+;;   (check-equal? (M `(record ''value) `(record 'value)) '())
+;;   (check-equal? (M `(record (capture ''value)) `(record ''value)) #f)
+
+;;   (check-equal? (q (CAPTURE 1)) `(capture 1))
+;;   (check-equal? (q (DISCARD)) `(discard))
+;;   (check-equal? (q `(capture 1)) `('capture 1))
+;;   (check-equal? (q `(discard)) `('discard))
+
+;;   )
diff --git a/unquoting.v b/unquoting.v
new file mode 100644
index 0000000..89ef60a
--- /dev/null
+++ b/unquoting.v
@@ -0,0 +1,1393 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String.
+Require Import Coq.Program.Equality.
+Require Import Coq.Arith.EqNat.
+Import ListNotations.
+Open Scope list_scope.
+Open Scope string_scope.
+Open Scope type_scope.
+
+Inductive label : Type := (* efficiency hack *)
+| lUnquote : label
+| lQuasiquote : label
+| lDiscard : label
+| lStr : string -> label.
+
+Inductive value : Type :=
+| vBool : bool -> value
+| vSymbol : label -> value
+| vRecord: value -> list value -> value
+| vSeq : list value -> value.
+
+Inductive pattern : nat -> Type :=
+| pBool : bool -> pattern 0
+| pSymbol : label -> pattern 0
+| pUnquote : forall n, pattern n -> pattern (S n)
+| pQuasiquote : forall n, pattern n -> pattern (pred n)
+| pRecord : forall n m, pattern n -> patseq m -> pattern (max n m)
+| pSeq : forall m, patseq m -> pattern m
+with patseq : nat -> Type :=
+| psNil : patseq 0
+| psCons : forall n m, pattern n -> patseq m -> patseq (max n m).
+
+Inductive command : Type :=
+| cDiscard : command
+| cQuasiquote : forall n, pattern n -> pred n = 0 -> command.
+
+Scheme Equality for label.
+
+Fixpoint value_ind'
+         (P : value -> Prop)
+         (PBool : forall b, P (vBool b))
+         (PSymbol : forall sym, P (vSymbol sym))
+         (PRecord : forall v vs, P v -> Forall P vs -> P (vRecord v vs))
+         (PSeq : forall vs, Forall P vs -> P (vSeq vs))
+         p
+         : P p.
+Proof.
+  induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ];
+    try solve [ induction l; [ apply Forall_nil | ];
+                apply Forall_cons; [ apply value_ind'; try assumption | ];
+                apply IHl ].
+Defined.
+
+Inductive psForall
+          (P : forall n, pattern n -> Prop)
+  : forall n, patseq n -> Prop :=
+| psfNil : psForall P 0 psNil
+| psfCons : forall n m p ps,
+    P n p -> psForall P m ps -> psForall P (max n m) (psCons n m p ps)
+.
+
+Fixpoint pattern_ind'
+         (P : forall n, pattern n -> Prop)
+         (PBool : forall b, P 0 (pBool b))
+         (PSymbol : forall sym, P 0 (pSymbol sym))
+         (PUnquote : forall n p, P n p -> P (S n) (pUnquote n p))
+         (PQuasiquote : forall n p, P n p -> P (pred n) (pQuasiquote n p))
+         (PRecord : forall n m p ps, P n p -> psForall P m ps -> P (max n m) (pRecord n m p ps))
+         (PSeq : forall m ps, psForall P m ps -> P m (pSeq m ps))
+         n
+         p
+  : P n p.
+Proof.
+  induction p; auto.
+
+  apply PRecord; [ apply IHp | ];
+    induction p0; [ apply psfNil | apply psfCons; [ apply pattern_ind' | ]; assumption ].
+
+  apply PSeq;
+    induction p; [ apply psfNil | apply psfCons; [ apply pattern_ind' | ]; assumption ].
+Defined.
+
+Definition unquote_count {n:nat} (p : pattern n) : nat :=
+  match p with
+  | pBool _ => 0
+  | pSymbol _ => 0
+  | pUnquote n _ => S n
+  | pQuasiquote n _ => pred n
+  | pRecord n m _ _ => max n m
+  | pSeq m _ => m
+  end.
+
+Definition unquote_count_seq {m:nat} (ps : patseq m) : nat :=
+  match ps with
+  | psNil => 0
+  | psCons n m _ _ => max n m
+  end.
+
+Lemma unquote_count_accurate : forall n (p : pattern n), unquote_count p = n.
+Proof.
+  destruct p; reflexivity.
+Defined.
+
+Lemma unquote_count_seq_accurate : forall n (ps : patseq n), unquote_count_seq ps = n.
+Proof.
+  destruct ps; reflexivity.
+Defined.
+
+Fixpoint parse v : option { n:nat & pattern n } :=
+  let parseSeq := (fix parseSeq vs : option { n:nat & patseq n } :=
+                     match vs with
+                     | [] => Some (existT patseq 0 psNil)
+                     | v :: vs' =>
+                       match parse v with
+                       | Some (existT _ n p) =>
+                         match parseSeq vs' with
+                         | Some (existT _ m ps') => Some (existT patseq (max n m) (psCons n m p ps'))
+                         | None => None
+                         end
+                       | None => None
+                       end
+                     end) in
+  match v with
+  | vBool b => Some (existT pattern 0 (pBool b))
+  | vSymbol l => Some (existT pattern 0 (pSymbol l))
+  | vRecord (vSymbol lUnquote) [v'] =>
+    match parse v' with
+    | Some (existT _ n p') => Some (existT pattern (S n) (pUnquote n p'))
+    | None => None
+    end
+  | vRecord (vSymbol lQuasiquote) [v'] =>
+    match parse v' with
+    | Some (existT _ n p') => Some (existT pattern (pred n) (pQuasiquote n p'))
+    | None => None
+    end
+  | vRecord v' vs =>
+    match parse v' with
+    | Some (existT _ n p') =>
+      match parseSeq vs with
+      | Some (existT _ m ps) => Some (existT pattern (max n m) (pRecord n m p' ps))
+      | None => None
+      end
+    | None => None
+    end
+  | vSeq vs =>
+    match parseSeq vs with
+    | Some (existT _ m ps) => Some (existT pattern m (pSeq m ps))
+    | None => None
+    end
+  end.
+
+Example parse1 :
+  parse (vBool true) =
+  Some (existT pattern 0 (pBool true)).
+reflexivity.
+Qed.
+
+Example parse2 :
+  parse (vRecord (vSymbol lDiscard) []) =
+  Some (existT pattern 0 (pRecord 0 0 (pSymbol lDiscard) psNil)).
+reflexivity.
+Qed.
+
+Example parse3 :
+  parse (vRecord (vSymbol lDiscard) [vBool true]) =
+  Some (existT pattern 0 (pRecord 0 0 (pSymbol lDiscard) (psCons 0 0 (pBool true) psNil))).
+reflexivity.
+Qed.
+
+Example parse4 :
+  parse (vRecord (vSymbol lUnquote) [vRecord (vSymbol lDiscard) []]) =
+  Some (existT pattern 1 (pUnquote 0 (pRecord 0 0 (pSymbol lDiscard) psNil))).
+reflexivity.
+Qed.
+
+Fixpoint unparse n (p : pattern n) : value :=
+  let unparseSeq := (fix unparseSeq m (ps : patseq m) : list value :=
+                       match ps with
+                       | psNil => []
+                       | psCons n m p ps' => unparse n p :: unparseSeq m ps'
+                       end) in
+  match p with
+  | pBool b => vBool b
+  | pSymbol l => vSymbol l
+  | pUnquote n p' => vRecord (vSymbol lUnquote) [unparse n p']
+  | pQuasiquote n p' => vRecord (vSymbol lQuasiquote) [unparse n p']
+  | pRecord n m p' ps => vRecord (unparse n p') (unparseSeq m ps)
+  | pSeq m ps => vSeq (unparseSeq m ps)
+  end.
+
+Definition parseSeq :=
+  (fix parseSeq vs : option { n:nat & patseq n } :=
+                     match vs with
+                     | [] => Some (existT patseq 0 psNil)
+                     | v :: vs' =>
+                       match parse v with
+                       | Some (existT _ n p) =>
+                         match parseSeq vs' with
+                         | Some (existT _ m ps') => Some (existT patseq (max n m) (psCons n m p ps'))
+                         | None => None
+                         end
+                       | None => None
+                       end
+                     end).
+
+Definition unparseSeq :=
+  (fix unparseSeq m (ps : patseq m) : list value :=
+     match ps with
+     | psNil => []
+     | psCons n m p ps' => unparse n p :: unparseSeq m ps'
+     end).
+
+Ltac destruct_useless_discriminant :=
+  match goal with
+  | hp:(Some _ = match ?e with | Some _ => _ | None => _ end) |- _ =>
+    destruct e as [[] | ]; simpl in hp
+  end.
+
+Ltac destruct_value v :=
+  let Hv := fresh "Heq" v in destruct v as [ | [] | | ] eqn: Hv using value_ind'.
+
+Ltac destruct_fields vs :=
+  let Hvs := fresh "Heq" vs in let vs0 := fresh vs in destruct vs as [ | ? vs0 ] eqn: Hvs; try destruct vs0.
+
+Ltac destruct_record v vs :=
+  destruct_value v; destruct_fields vs.
+
+Lemma unparseSeq_parseSeq_id vs :
+  forall m ps,
+    (Forall (fun v : value => forall (n : nat) (p : pattern n), Some (existT pattern n p) = parse v -> unparse n p = v) vs) ->
+    Some (existT patseq m ps) = parseSeq vs ->
+    unparseSeq m ps = vs.
+Proof.
+  induction vs; intros m ps Hvs Hlhs; [ inversion Hlhs; subst; simpl_existTs; subst; reflexivity | ];
+    destruct ps; [ simpl in Hlhs; repeat destruct_useless_discriminant; inversion Hlhs | ].
+  simpl; f_equal; simpl in Hlhs;
+    [ inversion Hvs; apply H1 |
+      apply IHvs; [ inversion Hvs; assumption | ] ];
+    repeat destruct_useless_discriminant;
+    inversion Hlhs; subst; simpl_existTs; subst; reflexivity.
+Qed.
+
+Lemma unparse_parse_id v :
+  forall n p,
+    Some (existT pattern n p) = parse v -> unparse n p = v.
+Proof.
+  induction v using value_ind'; intros n p Hlhs;
+    destruct p using pattern_ind';
+    fold parseSeq in * |- *;
+    try solve [ inversion Hlhs; reflexivity
+              | simpl in Hlhs; destruct_useless_discriminant; inversion Hlhs
+              | destruct_record v vs; simpl in Hlhs; repeat destruct_useless_discriminant; inversion Hlhs
+              | destruct_record v vs;
+                try solve [simpl in Hlhs; repeat destruct_useless_discriminant; inversion Hlhs];
+                simpl; repeat f_equal;
+                inversion H;
+                apply H2;
+                simpl in Hlhs; destruct_useless_discriminant;
+                inversion Hlhs; subst; simpl_existTs; subst; reflexivity ].
+
+  simpl; fold unparseSeq;
+    f_equal;
+    [ apply IHv |
+      apply unparseSeq_parseSeq_id; [ assumption | ];
+      simpl in Hlhs; fold parseSeq in Hlhs ];
+    destruct_record v vs; simpl in Hlhs; simpl;
+      try solve [ rewrite <- Heqvs in * |- *;
+                  repeat destruct_useless_discriminant;
+                  inversion Hlhs; subst; simpl_existTs; subst; reflexivity ].
+
+  simpl; fold unparseSeq; f_equal.
+  apply unparseSeq_parseSeq_id; [ assumption | ].
+  simpl in Hlhs; fold parseSeq in Hlhs.
+  destruct_useless_discriminant;
+    inversion Hlhs; subst; simpl_existTs; subst; reflexivity.
+Qed.
+
+Fixpoint compact n (p : pattern n) : { m:nat & pattern m } :=
+  let compactSeq := (fix compactSeq m ps : { m': nat & patseq m' } :=
+                       match ps with
+                       | psNil => existT patseq 0 psNil
+                       | psCons n m p ps =>
+                         let '(existT _ n p) := compact n p in
+                         let '(existT _ m ps) := compactSeq m ps in
+                         existT patseq (max n m) (psCons n m p ps)
+                       end) in
+  match p with
+  | pBool b => (existT pattern n p)
+  | pSymbol l => (existT pattern n p)
+  | pUnquote n p =>
+    let '(existT _ n p) := compact n p in
+    (existT pattern (S n) (pUnquote n p))
+  | pQuasiquote n p =>
+    let '(existT _ n p) := compact n p in
+    (existT pattern (pred n) (pQuasiquote n p))
+  | pRecord _ _ (pSymbol lUnquote) (psCons n _ p psNil) =>
+    let '(existT _ n p) := compact n p in
+    (existT pattern (S n) (pUnquote n p))
+  | pRecord _ _ (pSymbol lQuasiquote) (psCons n _ p psNil) =>
+    let '(existT _ n p) := compact n p in
+    (existT pattern (pred n) (pQuasiquote n p))
+  | pRecord n m p ps =>
+    let '(existT _ n p) := compact n p in
+    let '(existT _ m ps) := compactSeq m ps in
+    existT pattern (max n m) (pRecord n m p ps)
+  | pSeq m ps =>
+    let '(existT _ m ps) := compactSeq m ps in
+    existT pattern m (pSeq m ps)
+  end.
+
+Definition compactSeq :=
+  (fix compactSeq m ps : { m': nat & patseq m' } :=
+     match ps with
+     | psNil => existT patseq 0 psNil
+     | psCons n m p ps =>
+       let '(existT _ n p) := compact n p in
+       let '(existT _ m ps) := compactSeq m ps in
+       existT patseq (max n m) (psCons n m p ps)
+     end).
+
+Lemma parseSeq_unparseSeq_id m ps :
+  forall m' ps',
+    (psForall
+       (fun (n_uncompacted : nat) (p_uncompacted : pattern n_uncompacted) =>
+          forall (n : nat) (p : pattern n),
+            existT pattern n p = compact n_uncompacted p_uncompacted -> Some (existT pattern n p) = parse (unparse n p)) m ps) ->
+    existT patseq m' ps' = compactSeq m ps ->
+    Some (existT patseq m' ps') = parseSeq (unparseSeq m' ps').
+Proof.
+  induction ps; intros m' ps' Hps Hcompact.
+
+  inversion Hcompact; subst; simpl_existTs; subst.
+  reflexivity.
+
+  inversion Hps; subst; simpl_existTs; subst.
+  simpl in Hcompact.
+  destruct (compact n p).
+  destruct (compactSeq m ps).
+  inversion Hcompact; subst; simpl_existTs; subst.
+  simpl.
+  rewrite <- H2; auto.
+  rewrite <- IHps; auto.
+Qed.
+
+Ltac destruct_pattern p :=
+  let Hp := fresh "Heq" p in destruct p as [ | [] | | | | ] eqn: Hp using pattern_ind'.
+
+Ltac destruct_params ps :=
+  let Hps := fresh "Heq" ps in
+  let ps0 := fresh ps in
+  destruct ps as [ | ? ? ? ps0 ] eqn: Hps; try destruct ps0.
+
+Lemma parse_unparse_id n p :
+  forall nn pp,
+    existT pattern nn pp = compact n p ->
+    Some (existT pattern nn pp) = parse (unparse nn pp).
+Proof.
+  induction p using pattern_ind'; intros nn pp Hcompact;
+    try solve [ inversion Hcompact; subst; simpl_existTs; subst; reflexivity
+              | simpl in Hcompact;
+                destruct (compact n p);
+                inversion Hcompact; subst; simpl_existTs; subst;
+                simpl; rewrite <- IHp; reflexivity ];
+    try (dependent destruction p; destruct_all label);
+    try solve [
+          simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
+          destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
+          apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
+          inversion Hcompact; subst; simpl_existTs; subst;
+          simpl; fold parseSeq unparseSeq;
+          rewrite <- Heqps;
+          reflexivity ].
+
+  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
+    destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
+      remember Heqps as Heqps'; clear HeqHeqps';
+        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
+          destruct_params ps;
+          try solve [
+                inversion Hcompact; try subst nn; simpl_existTs; try subst pp;
+                simpl; fold parseSeq unparseSeq;
+                rewrite <- Heqps;
+                simpl in Heqps';
+                try destruct (compact n p0);
+                try destruct (compact n0 p1);
+                try destruct (compactSeq m ps0);
+                inversion Heqps'; subst; simpl_existTs; subst;
+                simpl;
+                reflexivity ];
+          (simpl in Heqps';
+           destruct (compact n p0) eqn: Heqp0; symmetry in Heqp0;
+           inversion Hcompact; subst; simpl_existTs; subst;
+           inversion H; subst; simpl_existTs; subst;
+           simpl;
+           rewrite <- H3; [ reflexivity | assumption ]).
+
+  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
+    destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
+      remember Heqps as Heqps'; clear HeqHeqps';
+        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
+          destruct_params ps;
+          try solve [
+                inversion Hcompact; try subst nn; simpl_existTs; try subst pp;
+                simpl; fold parseSeq unparseSeq;
+                rewrite <- Heqps;
+                simpl in Heqps';
+                try destruct (compact n p0);
+                try destruct (compact n0 p1);
+                try destruct (compactSeq m ps0);
+                inversion Heqps'; subst; simpl_existTs; subst;
+                simpl;
+                reflexivity ];
+          (simpl in Heqps';
+           destruct (compact n p0) eqn: Heqp0; symmetry in Heqp0;
+           inversion Hcompact; subst; simpl_existTs; subst;
+           inversion H; subst; simpl_existTs; subst;
+           simpl;
+           rewrite <- H3; [ reflexivity | assumption ]).
+
+  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
+    destruct (compact n p) eqn: Heqp; symmetry in Heqp;
+      assert (existT pattern (S x) (pUnquote x p0) = compact (S n) (pUnquote n p));
+      [ simpl; rewrite <- Heqp; reflexivity | ];
+      apply IHp in H0;
+      destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
+        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
+          inversion Hcompact; subst; simpl_existTs; subst;
+            simpl; fold parseSeq unparseSeq;
+              rewrite <- Heqps;
+              simpl in H0; rewrite <- H0; reflexivity.
+
+  simpl in Hcompact; fold parseSeq compactSeq in Hcompact;
+    destruct (compact n p) eqn: Heqp; symmetry in Heqp;
+      assert (existT pattern (pred x) (pQuasiquote x p0) = compact (pred n) (pQuasiquote n p));
+      [ simpl; rewrite <- Heqp; reflexivity | ];
+      apply IHp in H0;
+      destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps;
+        apply parseSeq_unparseSeq_id in Heqps; [ | assumption ];
+          inversion Hcompact; subst; simpl_existTs; subst;
+            simpl; fold parseSeq unparseSeq;
+              rewrite <- Heqps;
+              simpl in H0; rewrite <- H0; reflexivity.
+
+  assert (exists ln lp, existT pattern ln lp = compact (max n m0) (pRecord n m0 p p0)).
+  destruct (compact (max n m0) (pRecord n m0 p p0)) eqn: Hlabel.
+  exists x, p1.
+  reflexivity.
+  inversion H0 as [ln [lp Hlabel]].
+  remember Hlabel as Hlabel'; clear HeqHlabel'.
+  apply IHp in Hlabel.
+  simpl in Hcompact.
+  simpl in Hlabel'.
+  fold compactSeq in Hcompact, Hlabel'.
+  rewrite <- Hlabel' in Hcompact.
+  destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps.
+  apply parseSeq_unparseSeq_id in Heqps; [ | assumption ].
+  inversion Hcompact; subst; simpl_existTs; subst.
+  simpl; fold parseSeq unparseSeq.
+  rewrite <- Heqps.
+  rewrite <- Hlabel.
+  destruct (compact n p) eqn: Hnp.
+  destruct (compactSeq m0 p0) eqn: Hm0p0.
+  destruct_pattern p;
+    inversion Hlabel'; subst; simpl_existTs; subst; simpl; try reflexivity;
+      destruct p0; try destruct p0; try destruct (compact n p) eqn: Hnp2;
+        inversion Hlabel'; subst; simpl_existTs; subst; simpl; try reflexivity.
+
+  simpl in Hcompact; fold compactSeq in Hcompact.
+  simpl in IHp; fold compactSeq in IHp.
+  destruct (compactSeq m0 p) eqn: Hm0p; symmetry in Hm0p.
+  destruct (compactSeq m ps) eqn: Heqps; symmetry in Heqps.
+  apply parseSeq_unparseSeq_id in Heqps; [ | assumption ].
+  inversion Hcompact; subst; simpl_existTs; subst.
+  simpl; fold parseSeq unparseSeq.
+  rewrite <- Heqps.
+  replace (parseSeq (unparseSeq x p0)) with (Some (existT patseq x p0)); [ reflexivity | ].
+  apply (parseSeq_unparseSeq_id m0 p); [ | assumption ].
+  clear H Hcompact0 Heqps x0 p1 ps m.
+  dependent induction p; [ apply psfNil | apply psfCons ].
+
+  intros n0 p2 Hc.
+  simpl in Hm0p.
+  destruct (compact n p) eqn: Hnp.
+  destruct (compactSeq m p0) eqn: Hm0p2.
+  inversion Hm0p; subst; simpl_existTs; subst.
+  assert (Some (existT pattern (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p3 p4)))
+          = parse (unparse (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p3 p4))));
+    [ apply IHp0; reflexivity | ].
+  inversion Hc; subst; simpl_existTs; subst.
+  simpl in H; fold parseSeq unparseSeq in H.
+  destruct (parse (unparse x0 p3)) as [[]|] eqn: Hx0p3;
+    destruct (parseSeq (unparseSeq x1 p4)) as [[]|] eqn: Hx1p4;
+    inversion H; subst; simpl_existTs; subst; reflexivity.
+
+  simpl in Hm0p.
+  destruct (compact n p) eqn: Hnp.
+  destruct (compactSeq m p0) eqn: Hm0p2.
+  inversion Hm0p; subst; simpl_existTs; subst.
+  apply (IHp x1 p3); [ reflexivity | ].
+  intros.
+  inversion H; subst; simpl_existTs; subst.
+  assert (Some (existT pattern (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p2 p3)))
+          = parse (unparse (Nat.max x0 x1) (pSeq (Nat.max x0 x1) (psCons x0 x1 p2 p3))));
+    [ apply IHp0; reflexivity | ].
+  simpl in H; fold parseSeq unparseSeq in H.
+  simpl; fold parseSeq unparseSeq.
+  destruct (parseSeq (unparseSeq x1 p3)) as [[]|];
+    destruct (parse (unparse x0 p2)) as [[]|];
+    inversion H; subst; simpl_existTs; subst; reflexivity.
+Qed.
+
+Fixpoint mat n p v level : bool :=
+  let matSeq := (fix matSeq m ps vs level : bool :=
+                   match ps, vs with
+                   | psNil, [] => true
+                   | psCons n' m' p' ps', (v' :: vs') => andb (mat n' p' v' level) (matSeq m' ps' vs' level)
+                   | _, _ => false
+                   end) in
+  match p with
+  | pBool b =>
+    match v with
+    | vBool b0 => bool_beq b b0
+    | _ => false
+    end
+  | pSymbol l =>
+    match v with
+    | vSymbol l0 => label_beq l l0
+    | _ => false
+    end
+  | pUnquote n' p' =>
+    match level with
+    | 0 =>
+      match p' with
+      | pQuasiquote n'' p'' => mat n'' p'' v 0
+      | pRecord _ _ (pSymbol lDiscard) psNil => true
+      | _ => (* unreachable unless bogus commands present *) false
+      end
+    | S level' =>
+      match v with
+      | vRecord (vSymbol lUnquote) [v'] =>
+        mat n' p' v' level'
+      | _ => false
+      end
+    end
+  | pQuasiquote n' p' =>
+    match v with
+    | vRecord (vSymbol lQuasiquote) [v'] =>
+      mat n' p' v' (S level)
+    | _ => false
+    end
+  | pRecord n' m' p' ps' =>
+    match v with
+    | vRecord v vs => andb (mat n' p' v level) (matSeq m' ps' vs level)
+    | _ => false
+    end
+  | pSeq m' ps' =>
+    match v with
+    | vSeq vs' => matSeq m' ps' vs' level
+    | _ => false
+    end
+  end.
+
+Fixpoint well_formed n (p : pattern n) level : Prop :=
+  let well_formedSeq := (fix well_formedSeq m ps level : Prop :=
+                           match ps with
+                           | psNil => True
+                           | psCons n' m' p' ps' =>
+                             well_formed n' p' level /\ well_formedSeq m' ps' level
+                           end) in
+  match p with
+  | pBool _ => True
+  | pSymbol _ => True
+  | pUnquote n' p' =>
+    match level with
+    | 0 =>
+      match p' with
+      | pQuasiquote n'' p'' => well_formed n'' p'' 0
+      | pRecord _ _ (pSymbol lDiscard) psNil => True
+      | _ => False
+      end
+    | S level' =>
+      well_formed n' p' level'
+    end
+  | pQuasiquote n' p' =>
+    well_formed n' p' (S level)
+  | pRecord n' m' p' ps' =>
+    well_formed n' p' level /\ well_formedSeq m' ps' level
+  | pSeq m' ps' =>
+    well_formedSeq m' ps' level
+  end.
+
+Definition is_compact n (p : pattern n) : Prop :=
+  (existT pattern n p) = compact n p.
+
+Lemma compactness_of_parseSeq vs :
+  forall m ps,
+    (Forall
+       (fun v : value =>
+          forall (n : nat) (p : pattern n),
+            Some (existT pattern n p) = parse v -> is_compact n p) vs) ->
+    Some (existT patseq m ps) = parseSeq vs ->
+    psForall is_compact m ps.
+Proof.
+  induction vs; intros m ps Hvs Hparse;
+    inversion Hparse; subst; simpl_existTs; subst.
+  apply psfNil.
+  inversion Hvs;
+    destruct (parse a) as [[]|] eqn: Ha; [ | congruence ];
+      destruct (parseSeq vs) as [[]|] eqn: Hvs'; [ | congruence ];
+        inversion H0; subst; simpl_existTs; subst;
+          apply psfCons; [ apply H2; reflexivity
+                         | apply IHvs; [ assumption | reflexivity ] ].
+Qed.
+
+Lemma convert_compactSeq:
+  forall m ps,
+    psForall is_compact m ps -> existT patseq m ps = compactSeq m ps.
+Proof.
+  induction ps; intros Hlhs.
+  reflexivity.
+  inversion Hlhs; subst; simpl_existTs; subst.
+  simpl.
+  unfold is_compact in H2; rewrite <- H2.
+  apply IHps in H6; rewrite <- H6.
+  reflexivity.
+Qed.
+
+Lemma compactness_of_parse v :
+  forall n p,
+    Some (existT pattern n p) = parse v ->
+    is_compact n p.
+Proof.
+  induction v using value_ind'; intros n p Hlhs;
+    try solve [inversion Hlhs; subst; simpl_existTs; subst; reflexivity].
+
+  destruct_value v.
+
+  simpl in Hlhs; fold parseSeq in Hlhs;
+    (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | congruence ]);
+    (apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
+    apply convert_compactSeq in H;
+    inversion Hlhs; subst; simpl_existTs; subst;
+      unfold is_compact; simpl; fold compactSeq;
+        rewrite <- H;
+        reflexivity.
+
+  admit.
+  admit.
+  admit.
+
+  simpl in Hlhs; fold parseSeq in Hlhs;
+    (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | congruence ]);
+    (apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
+    apply convert_compactSeq in H;
+    inversion Hlhs; subst; simpl_existTs; subst;
+      unfold is_compact; simpl; fold compactSeq;
+        rewrite <- H;
+        reflexivity.
+
+  simpl in Hlhs; fold parseSeq in Hlhs.
+  destruct (parse v) as [[n' p']|] eqn: Hv'.
+  rewrite Heqv in Hv'; simpl in Hv'; fold parseSeq in Hv'.
+  rewrite Hv' in Hlhs.
+  (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | congruence ]);
+    (apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
+    apply convert_compactSeq in H;
+    inversion Hlhs; subst; simpl_existTs; subst;
+      unfold is_compact; simpl; fold compactSeq;
+        rewrite <- H.
+  symmetry in Hv'.
+  apply IHv in Hv'.
+  unfold is_compact in Hv'.
+  rewrite <- Hv'.
+
+
+
+  destruct_fields vs;
+    simpl in Hlhs; fold parseSeq in Hlhs;
+    rewrite <- Heqvs in * |- *;
+      (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | try congruence ]);
+      try ((apply (compactness_of_parseSeq vs m ps) in H; [ | symmetry; assumption ]);
+           apply convert_compactSeq in H;
+           inversion Hlhs; subst; simpl_existTs; subst;
+           unfold is_compact; simpl; fold compactSeq;
+           rewrite <- H;
+           reflexivity).
+  admit.
+  admit.
+
+
+
+  destruct_value v;
+    (simpl in Hlhs; fold parseSeq in Hlhs;
+     destruct_fields vs;
+     try rewrite <- Heqvs in H;
+     try rewrite <- Heqvs in Hlhs;
+     (destruct (parseSeq vs) as [[m ps]|] eqn: Hvs; [ | try congruence ]);
+     try (apply (compactness_of_parseSeq vs m ps) in H;
+          [ | symmetry; assumption ];
+          apply convert_compactSeq in H);
+     inversion Hlhs; subst; simpl_existTs; subst;
+     unfold is_compact; simpl; fold compactSeq;
+     inversion Hvs;
+     try (destruct (parse v0) as [[]|]; [ | congruence ]);
+     try inversion H1; try inversion H2;
+     subst; simpl_existTs; subst;
+     try (rewrite <- H));
+    try solve [ reflexivity
+              | inversion H as [Hp0]; simpl; destruct (compact x p0);
+                inversion Hp0; subst; simpl_existTs; subst;
+                reflexivity ].
+
+
+  admit.
+  simpl.
+  reflexivity.
+
+(* STOP DELETING, the vSeq case follows *)
+
+  simpl in Hlhs; fold parseSeq in Hlhs.
+  destruct (parseSeq vs) as [[]|] eqn: Hvs; [ | congruence ].
+  inversion Hlhs; subst; simpl_existTs; subst.
+  unfold is_compact; simpl; fold compactSeq.
+  apply (compactness_of_parseSeq vs x p0) in H.
+  rewrite <- convert_compactSeq; [ reflexivity | assumption ].
+  symmetry; assumption.
+
+  destruct_value v;
+    try solve [inversion Hlhs; subst; simpl_existTs; subst; reflexivity].
+
+
+  (Forall
+     (fun v : value =>
+        forall (n : nat) (p : pattern n),
+          Some (existT pattern n p) = parse v -> is_compact n p) vs) ->
+  
+  b : bool
+  Heqv : v = vBool b
+  IHv : forall (n : nat) (p : pattern n),
+        Some (existT pattern n p) = parse (vBool b) -> is_compact n p
+  n : nat
+  p : pattern n
+  Hlhs : Some (existT pattern n p) = parse (vRecord (vBool b) vs)
+
+
+
+  simpl in Hlhs; fold parseSeq in Hlhs.
+  unfold is_compact in IHp; rewrite <- IHp.
+  reflexivity.
+  
+
+Theorem quotation_invariant v :
+  forall ,
+    Some (existT pattern n p) = parse v ->
+    
+
+Ltac flatten_conj :=
+  match goal with
+  | hp:(?x /\ ?y) |- _ =>
+    let hp1 := fresh hp in
+    let hp2 := fresh hp in
+    inversion hp as [hp1 hp2]; clear hp
+  end.
+
+Lemma quotation_invariant_lit s :
+  forall v level,
+    value_size v = s ->
+    wellFormedLit level v ->
+    (forall u, matLit (S level) v u = Some true <-> u = v).
+Proof.
+  induction s using Wf_nat.lt_wf_ind; intros v level Hs Hwf u.
+
+  destruct v; split; intro Hlhs; destruct u; try solve [inversion Hlhs].
+
+  inversion Hlhs as [Hlhs']; apply internal_bool_dec_bl in Hlhs'; subst; reflexivity.
+  rewrite Hlhs; simpl; rewrite internal_bool_dec_lb; reflexivity.
+
+  inversion Hlhs as [Hlhs']; apply internal_label_dec_bl in Hlhs'; subst; reflexivity.
+  rewrite Hlhs; simpl; rewrite internal_label_dec_lb; reflexivity.
+
+  destruct v; destruct_all label; do 2 (try destruct l); inversion Hlhs; inversion Hwf.
+  destruct v; destruct_all label; do 2 (try destruct l); inversion Hlhs; inversion Hwf.
+
+  destruct v; destruct_all label; do 2 (try destruct l);
+    destruct u; destruct_all label; do 2 (try destruct l0).
+
+      try congruence;
+      try (apply optand_Some_true in Hlhs'; flatten_conj).
+  apply H with (m := 0) in Hlhs'0.
+
+      inversion Hlhs'; try inversion Hwf.
+  f_equal; f_equal.
+  rewrite <- quotation_invariant_lit with (level := 0) (s := value_size v).
+  assumption.
+  reflexivity.
+
+Lemma qSeq : forall level l,
+    (forall (level : nat) (v : value),
+        wellFormedLit level v -> forall u : value, matLit (S level) v u = Some true <-> u = v) ->
+    (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
+       match ps with
+       | [] => True
+       | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
+       end) level l ->
+    forall l0,
+      ((fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
+          match ps with
+          | [] => match vs with
+                  | [] => Some true
+                  | _ :: _ => Some false
+                  end
+          | p :: ps' => match vs with
+                        | [] => Some false
+                        | v :: vs' => optand (matLit level p v) (matList level ps' vs')
+                        end
+          end) (S level) l l0 = Some true) <-> l = l0.
+Proof.
+  intros level l Hquotation_invariant_lit Hwf; dependent induction l; destruct l0;
+    split; try congruence; intro Hlhs.
+
+  inversion_clear Hwf as [Hwfa Hwfl].
+  apply optand_Some_true in Hlhs; inversion_clear Hlhs as [Hmatav Hmatll0].
+  apply Hquotation_invariant_lit in Hmatav; [ | assumption ]; rewrite Hmatav in * |- *; clear Hmatav.
+  f_equal.
+  apply IHl; assumption.
+
+  inversion Hlhs; subst.
+  inversion_clear Hwf as [Hwfv Hwfl0].
+  apply optand_Some_true; split.
+  apply Hquotation_invariant_lit; try assumption; reflexivity.
+  apply IHl; try assumption; reflexivity.
+Qed.
+
+Lemma matLit_true :
+  forall level v,
+    (forall (level : nat) (v : value),
+        wellFormedLit level v -> forall u : value, matLit (S level) v u = Some true <-> u = v) ->
+    wellFormedLit level v -> matLit (S level) v v = Some true.
+Proof.
+  intros; apply H; [ assumption | reflexivity ].
+Defined.
+
+Lemma matList_true :forall level l,
+    (forall (level : nat) (v : value),
+        wellFormedLit level v -> forall u : value, matLit (S level) v u = Some true <-> u = v) ->
+    (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
+       match ps with
+       | [] => True
+       | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
+       end) level l ->
+    (fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
+       match ps with
+       | [] => match vs with
+               | [] => Some true
+               | _ :: _ => Some false
+               end
+       | p :: ps' => match vs with
+                     | [] => Some false
+                     | v :: vs' => optand (matLit level p v) (matList level ps' vs')
+                     end
+       end) (S level) l l = Some true.
+Proof.
+  intros; apply qSeq; auto.
+Defined.
+
+Fixpoint quotation_invariant v :
+  wellFormed v -> (forall u, mat (vQuasiquote v) u = Some true <-> u = v)
+with quotation_invariant_lit level v :
+  wellFormedLit level v -> (forall u, matLit (S level) v u = Some true <-> u = v).
+Proof.
+  (* quotation_invariant *)
+
+  destruct v; intros Hwf u; split; intro Hlhs; try solve [inversion Hwf].
+
+  destruct u; destruct v; destruct_all label; try inversion Hwf;
+    try solve [do 2 (try destruct l); simpl in Hlhs; congruence];
+    (do 2 (try destruct l; try inversion Hwf);
+     destruct u; do 2 (try destruct l0); destruct_all label; simpl in Hlhs; try congruence;
+     (apply quotation_invariant_lit in Hlhs; [ subst; reflexivity | ];
+      simpl in Hwf); assumption).
+
+  destruct u; destruct v; destruct_all label; try inversion Hwf;
+    try solve [do 2 (try destruct l); simpl in Hlhs; congruence];
+    (do 2 (try destruct l; try inversion Hwf);
+     destruct u; do 2 (try destruct l0); destruct_all label; simpl in Hlhs; try congruence);
+    [ apply quotation_invariant_lit; [ simpl in Hwf; assumption | ];
+      inversion Hlhs; reflexivity
+    | reflexivity ].
+
+  (* quotation_invariant_lit *)
+
+  destruct v; intros Hwf u; split; intro Hlhs.
+
+  destruct u; inversion Hlhs; apply internal_bool_dec_bl in H0; subst; auto.
+  inversion Hlhs; simpl; rewrite internal_bool_dec_lb; reflexivity.
+
+  destruct u; inversion Hlhs; apply internal_label_dec_bl in H0; subst; auto.
+  inversion Hlhs; simpl; rewrite internal_label_dec_lb; reflexivity.
+
+  destruct u;
+    try solve [destruct v; destruct_all label; do 2 (try destruct l); simpl in Hlhs; congruence];
+    remember v as v'; destruct v; rewrite Heqv' in Hwf, Hlhs;
+      (assert (wellFormedLit level v'); [rewrite Heqv'; try solve [reflexivity | inversion Hwf; assumption] | ];
+       apply quotation_invariant_lit with (u := u) in H;
+       destruct_all label;
+       try (apply optand_Some_true in Hlhs; inversion Hlhs as [Hlhsv Hlhsl]; clear Hlhs;
+            rewrite Heqv' in H; simpl in H;
+            apply H in Hlhsv; subst;
+            f_equal;
+            inversion_clear Hwf as [Hwfv Hwfl];
+            symmetry; apply (qSeq level); try assumption)).
+
+  admit.
+  admit.
+
+
+  subst; destruct v; destruct_all label; do 2 (try destruct l); try (simpl; reflexivity);
+    try solve [ simpl in Hwf; repeat flatten_conj;
+                repeat (simpl; rewrite matLit_true; auto);
+                repeat (simpl; rewrite matList_true; auto);
+                try solve [ simpl; rewrite internal_bool_dec_lb; reflexivity
+                          | simpl; rewrite internal_string_dec_lb; reflexivity ]
+              | replace (matLit (S level) (vRecord (vRecord v l0) []) (vRecord (vRecord v l0) []))
+                with (optand (matLit (S level) (vRecord v l0) (vRecord v l0)) (Some true)); [ | reflexivity ];
+                simpl in Hwf; repeat flatten_conj;
+                rewrite matLit_true; auto;
+                repeat (split; try assumption) ].
+
+  destruct level; simpl in Hwf; [ | simpl; rewrite matLit_true; auto ].
+  destruct v; try solve [inversion Hwf];
+    destruct v; try solve [inversion Hwf];
+      destruct l0; try solve [inversion Hwf];
+        do 2 (try destruct l); try solve [inversion Hwf].
+  apply quotation_invariant with (u := (vRecord (vSymbol lQuasiquote) [v])) in Hwf.
+  simpl in Hwf.
+  simpl.
+
+  Lemma matList_S vs level :
+    (Forall (fun v : value => matLit level v v = Some true -> matLit (S level) v v = Some true) vs) ->
+    (fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
+       match ps with
+       | [] => match vs with
+               | [] => Some true
+               | _ :: _ => Some false
+               end
+       | p :: ps' => match vs with
+                     | [] => Some false
+                     | v :: vs' => optand (matLit level p v) (matList level ps' vs')
+                     end
+       end) level vs vs = Some true ->
+    (fix matList (level0 : nat) (ps vs0 : list value) {struct ps} : option bool :=
+       match ps with
+       | [] => match vs0 with
+               | [] => Some true
+               | _ :: _ => Some false
+               end
+       | p :: ps' => match vs0 with
+                     | [] => Some false
+                     | v :: vs' => optand (matLit level0 p v) (matList level0 ps' vs')
+                     end
+       end) (S level) vs vs = Some true.
+  Proof.
+    induction vs; intros; [ reflexivity | ].
+    inversion H.
+    apply optand_Some_true in H0; flatten_conj.
+    apply optand_Some_true.
+    split.
+    apply H3.
+    assumption.
+    apply IHvs.
+    assumption.
+    assumption.
+  Qed.
+
+  Lemma useless_match : forall A (v : option A),
+      match v with | Some v' => Some v' | None => None end = v.
+  Proof.
+    destruct v; reflexivity.
+  Qed.
+
+  Lemma matLit_S_SS : forall level v,
+      matLit (S level) v v = Some true ->
+      matLit (S (S level)) v v = Some true.
+  Proof.
+    induction v using value_ind'; intro Hlhs;
+      [ simpl; rewrite internal_bool_dec_lb; reflexivity
+      | simpl; rewrite internal_label_dec_lb; reflexivity
+      |
+      | apply matList_S; assumption ].
+    dependent induction v.
+    simpl in Hlhs |- *;
+      rewrite matList_S; [ rewrite internal_bool_dec_lb; reflexivity
+                         | assumption
+                         | rewrite internal_bool_dec_lb in Hlhs; [ | reflexivity ]; simpl in Hlhs;
+                           rewrite useless_match in Hlhs; assumption ].
+
+    destruct l; do 2 (try destruct vs); try (simpl in * |- *; reflexivity).
+
+    inversion H; apply H2; apply Hlhs.
+
+    simpl in Hlhs |- *; rewrite useless_match; rewrite useless_match in Hlhs.
+    apply optand_Some_true in Hlhs; flatten_conj.
+    apply optand_Some_true in Hlhs1; flatten_conj.
+    inversion H.
+    inversion H3.
+    subst.
+    apply optand_Some_true; split; [ apply H2; assumption | ].
+    apply optand_Some_true; split; [ apply H6; assumption | ].
+    apply matList_S; assumption.
+
+    
+      rewrite matList_S; [ rewrite internal_label_dec_lb; reflexivity
+                         | assumption
+                         | rewrite internal_label_dec_lb in Hlhs; [ | reflexivity ]; simpl in Hlhs;
+                           rewrite useless_match in Hlhs; assumption ].
+  Qed.
+
+  apply quotation_invariant_lit; [ | reflexivity ].
+
+
+  (****** STOP DELETING *)
+
+  destruct u; inversion Hlhs; clear Hlhs;
+    f_equal; symmetry; apply (qSeq level); try assumption.
+  inversion Hlhs; simpl; apply (qSeq level); try assumption; reflexivity.
+Qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Lemma qSeq : forall level l,
+    (forall (level : nat) (v : value),
+        wellFormedLit level v -> forall u : value, matLit level v u = Some true <-> u = v) ->
+    (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
+       match ps with
+       | [] => True
+       | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
+       end) level l ->
+    forall l0,
+      ((fix matList (level : nat) (ps vs : list value) {struct ps} : option bool :=
+          match ps with
+          | [] => match vs with
+                  | [] => Some true
+                  | _ :: _ => Some false
+                  end
+          | p :: ps' => match vs with
+                        | [] => Some false
+                        | v :: vs' => optand (matLit level p v) (matList level ps' vs')
+                        end
+          end) level l l0 = Some true) <-> l = l0.
+Proof.
+  intros level l Hquotation_invariant_lit Hwf; dependent induction l; destruct l0;
+    split; try congruence; intro Hlhs.
+
+  inversion_clear Hwf as [Hwfa Hwfl].
+  apply optand_Some_true in Hlhs; inversion_clear Hlhs as [Hmatav Hmatll0].
+  apply Hquotation_invariant_lit in Hmatav; [ | assumption ]; rewrite Hmatav in * |- *; clear Hmatav.
+  f_equal.
+  apply IHl; assumption.
+
+  inversion Hlhs; subst.
+  inversion_clear Hwf as [Hwfv Hwfl0].
+  apply optand_Some_true; split.
+  apply Hquotation_invariant_lit; try assumption; reflexivity.
+  apply IHl; try assumption; reflexivity.
+Qed.
+
+(* Lemma wfList_S : *)
+(*   forall l level, *)
+(*     (forall (v : value) (level : nat), wellFormedLit level v -> wellFormedLit (S level) v) -> *)
+(*     (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop := *)
+(*        match ps with *)
+(*        | [] => True *)
+(*        | p :: ps' => wellFormedLit level p /\ wellFormedList level ps' *)
+(*        end) level l -> *)
+(*     (fix wellFormedList (level0 : nat) (ps : list value) {struct ps} : Prop := *)
+(*        match ps with *)
+(*        | [] => True *)
+(*        | p :: ps' => wellFormedLit level0 p /\ wellFormedList level0 ps' *)
+(*        end) (S level) l. *)
+(* Proof. *)
+(*   induction l; intros; [ reflexivity | ]. *)
+(*   inversion H0; split. *)
+(*   apply H in H1; assumption. *)
+(*   apply IHl; assumption. *)
+(* Qed. *)
+
+Lemma wfList_S vs level :
+  (Forall (fun v : value => wellFormedLit level v -> wellFormedLit (S level) v) vs) ->
+  (fix wellFormedList (level : nat) (ps : list value) {struct ps} : Prop :=
+     match ps with
+     | [] => True
+     | p :: ps' => wellFormedLit level p /\ wellFormedList level ps'
+     end) level vs ->
+  (fix wellFormedList (level0 : nat) (ps : list value) {struct ps} : Prop :=
+     match ps with
+     | [] => True
+     | p :: ps' => wellFormedLit level0 p /\ wellFormedList level0 ps'
+     end) (S level) vs.
+Proof.
+  induction vs; intros; [ reflexivity | ].
+  inversion H0; split.
+  inversion H.
+  apply H5 in H1.
+  assumption.
+  apply IHvs.
+  inversion H; assumption.
+  assumption.
+Qed.
+
+Lemma wfLit_S v level :
+  wellFormedLit level v -> wellFormedLit (S level) v.
+Proof.
+  induction v using value_ind'; intros; try reflexivity.
+
+  destruct v; destruct_all label.
+
+  inversion_clear H0 as [H1 H2].
+  split; [ reflexivity | ].
+  apply wfList_S; assumption.
+
+  do 2 (try destruct vs).
+  split; reflexivity.
+  inversion H.
+  simpl in H0.
+  destruct level.
+  simpl.
+
+  Lemma wf0 v : wellFormed v -> forall level, wellFormedLit level v.
+  Proof.
+    induction v using value_ind'; try reflexivity; intro Hlhs.
+    destruct v; try inversion Hlhs.
+    destruct l; try inversion Hlhs.
+    do 2 (try destruct vs); try inversion Hlhs.
+    simpl in Hlhs |- *.
+
+    induction level; [ | ].
+
+
+    dependent destruction v; try reflexivity.
+    dependent destruction v; try inversion Hlhs.
+    split; [ reflexivity | apply wfList_S ].
+    destruct_all label.
+    do 2 (try destruct vs).
+    split; reflexivity.
+    inversion H; apply H2.
+    simpl in Hlhs.
+
+    split; [ reflexivity | ].
+
+  
+  inversion H.
+  destruct v; try reflexivity.
+  destruct v; try inversion H.
+  destruct_all label; try inversion H.
+  do 2 (try destruct l); try inversion H.
+  simpl; apply wfLit_S; assumption.
+  destruct l.
+  split; reflexivity.
+  inversion H.
+
+  inversion H.
+
+  simpl in H |- *; apply wfLit_S; assumption.
+  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
+  split; [ reflexivity | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  apply wfList_S; assumption.
+
+  do 2 (try destruct l).
+  split; reflexivity.
+  simpl in H |- *; apply wfLit_S; assumption.
+  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
+  split; [ reflexivity | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  apply wfList_S; assumption.
+
+  destruct l.
+  split; reflexivity.
+  simpl in H |- *; inversion_clear H as [H0 [H1 H2]].
+  split; [ reflexivity | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  apply wfList_S; assumption.
+
+  inversion_clear H as [H0 H1].
+  split; [ reflexivity | ].
+  apply wfList_S; assumption.
+
+  inversion_clear H as [H0 H1].
+  split.
+  apply wfLit_S; assumption.
+  apply wfList_S; assumption.
+
+  inversion_clear H as [H0 H1].
+  split.
+  apply wfLit_S; assumption.
+  apply wfList_S; assumption.
+
+  apply wfList_S; assumption.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+  destruct v; intros; try reflexivity.
+
+  destruct v; destruct_all label.
+
+  (* split; [ reflexivity | ]; apply wfList_S; [ apply wfLit_S | ]; *)
+  (*   inversion H; assumption. *)
+  inversion_clear H as [H0 H1].
+  split; [ reflexivity | ].
+  apply wfList_S; assumption.
+
+  do 2 (try destruct l).
+  split; reflexivity.
+  destruct level.
+  simpl in H |- *; apply wfLit_S.
+  destruct v; try reflexivity.
+  destruct v; try inversion H.
+  destruct_all label; try inversion H.
+  do 2 (try destruct l); try inversion H.
+  simpl; apply wfLit_S; assumption.
+  destruct l.
+  split; reflexivity.
+  inversion H.
+
+  inversion H.
+
+  simpl in H |- *; apply wfLit_S; assumption.
+  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
+  split; [ reflexivity | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  apply wfList_S; assumption.
+
+  do 2 (try destruct l).
+  split; reflexivity.
+  simpl in H |- *; apply wfLit_S; assumption.
+  simpl in H |- *; inversion_clear H as [H0 [H1 [H2 H3]]].
+  split; [ reflexivity | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  apply wfList_S; assumption.
+
+  destruct l.
+  split; reflexivity.
+  simpl in H |- *; inversion_clear H as [H0 [H1 H2]].
+  split; [ reflexivity | ].
+  split; [ simpl; apply wfLit_S; assumption | ].
+  apply wfList_S; assumption.
+
+  inversion_clear H as [H0 H1].
+  split; [ reflexivity | ].
+  apply wfList_S; assumption.
+
+  inversion_clear H as [H0 H1].
+  split.
+  apply wfLit_S; assumption.
+  apply wfList_S; assumption.
+
+  inversion_clear H as [H0 H1].
+  split.
+  apply wfLit_S; assumption.
+  apply wfList_S; assumption.
+
+  apply wfList_S; assumption.
+
+
+Defined.
+
+Fixpoint quotation_invariant v :
+  wellFormed v -> (forall u, mat (vQuasiquote v) u = Some true <-> u = v)
+with quotation_invariant_lit level v :
+  wellFormedLit level v -> (forall u, matLit level v u = Some true <-> u = v).
+Proof.
+  (* quotation_invariant *)
+
+  destruct v; intros Hwf u; split; intro Hlhs; try solve [inversion Hwf].
+
+  destruct u; destruct v; destruct_all label; try inversion Hwf;
+    try solve [do 2 (try destruct l); simpl in Hlhs; congruence];
+    (do 2 (try destruct l; try inversion Hwf);
+     destruct u; do 2 (try destruct l0); destruct_all label; simpl in Hlhs; try congruence;
+     (apply quotation_invariant_lit in Hlhs; [ subst; reflexivity | ];
+      simpl in Hwf)).
+
+
+  destruct u; inversion_clear Hlhs; destruct v; destruct_all label; try inversion Hwf;
+    do 2 (try destruct l); try inversion Hwf;
+      [ apply quotation_invariant_lit; [ apply Hwf | reflexivity ] | reflexivity ].
+
+  (* quotation_invariant_lit *)
+
+  destruct v; intros Hwf u; split; intro Hlhs.
+
+  destruct u; inversion Hlhs; apply internal_bool_dec_bl in H0; subst; auto.
+  inversion Hlhs; simpl; rewrite internal_bool_dec_lb; reflexivity.
+
+  destruct u; inversion Hlhs; apply internal_label_dec_bl in H0; subst; auto.
+  inversion Hlhs; simpl; rewrite internal_label_dec_lb; reflexivity.
+
+  destruct u;
+    try solve [destruct v; destruct_all label; do 2 (try destruct l); simpl in Hlhs; congruence];
+    remember v as v'; destruct v; rewrite Heqv' in Hwf, Hlhs;
+      (assert (wellFormedLit level v'); [rewrite Heqv'; try solve [reflexivity | inversion Hwf; assumption] | ];
+       apply quotation_invariant_lit with (u := u) in H;
+       destruct_all label;
+       try (apply optand_Some_true in Hlhs; inversion Hlhs as [Hlhsv Hlhsl]; clear Hlhs;
+            rewrite Heqv' in H; simpl in H;
+            apply H in Hlhsv; subst;
+            f_equal;
+            inversion_clear Hwf as [Hwfv Hwfl];
+            symmetry; apply (qSeq level); try assumption)).
+
+  admit.
+  admit.
+
+  subst; destruct v; destruct_all label.
+
+  inversion Hwf.
+  assert (l = l) as Hll; [ reflexivity | ];
+    apply (qSeq level) in Hll; try assumption.
+  simpl; rewrite Hll.
+  f_equal; apply andb_true_intro; split; try destruct b; reflexivity.
+
+  do 2 (try destruct l).
+  reflexivity.
+  simpl in * |- *.
+  inversion Hwf.
+  assert (l = l) as Hll; [ reflexivity | ];
+    apply (qSeq level) in Hll; try assumption.
+  simpl; rewrite Hll.
+  f_equal; apply andb_true_intro; split; try destruct b; reflexivity.
+
+  apply (qSeq level) with (l0 := l) in H0.
+
+  assert (l = l) as Hll; [ reflexivity | ].
+  apply (qSeq level) in Hll.
+  admit.
+  assumption.
+  destruct v; destruct_all label; try solve [inversion Hwf; assumption].
+  destruct l; try destruct l; simpl in Hwf.
+  reflexivity.
+  
+
+  do 2 (try destruct l); try reflexivity.
+  admit.
+  admit.
+
+  (************** STOP DELETING *)
+
+  destruct u; inversion Hlhs; clear Hlhs;
+    f_equal; symmetry; apply (qSeq level); try assumption.
+  inversion Hlhs; simpl; apply (qSeq level); try assumption; reflexivity.
+Qed.