diff --git a/quoting.rkt b/quoting.rkt
new file mode 100644
index 0000000..317b651
--- /dev/null
+++ b/quoting.rkt
@@ -0,0 +1,103 @@
+#lang racket
+
+(require racket/trace)
+
+(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 '()))]))
+
+;; (trace m)
+
+(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/quoting.v b/quoting.v
new file mode 100644
index 0000000..4cc517d
--- /dev/null
+++ b/quoting.v
@@ -0,0 +1,166 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Program.Equality.
+Require Import Omega.
+Require Import String.
+Require Import Bool.
+Import ListNotations.
+Open Scope list_scope.
+Open Scope string_scope.
+
+Inductive label : Type := (* efficiency hack *)
+| lDiscard : label
+| lCapture : label
+| lQuote: label
+| lStr : string -> label.
+
+Inductive value : Type :=
+| vBool : bool -> value
+| vSymbol : label -> value
+| vRecord: value -> values -> value
+| vSeq : values -> value
+with values : Type :=
+     | vsNil : values
+     | vsCons : value -> values -> values.
+
+Inductive pat : Type :=
+| pDiscard : pat
+| pCapture : pat -> pat
+| pBool : bool -> pat
+| pSymbol : label -> pat
+| pRecord: pat -> pats -> pat
+| pSeq : pats -> pat
+with pats : Type :=
+     | psNil : pats
+     | psCons : pat -> pats -> pats.
+
+Definition vs1 v : values := vsCons v vsNil.
+Definition ps1 p : pats := psCons p psNil.
+
+Definition vQuote v : value := vRecord (vSymbol lQuote) (vs1 v).
+
+Lemma value_dec : forall x y : value, { x = y } + { x <> y }
+with values_dec : forall xs ys : values, { xs = ys } + { xs <> ys }.
+  repeat decide equality.
+  repeat decide equality.
+Defined.
+
+Lemma pat_dec : forall x y : pat, { x = y } + { x <> y }
+with pats_dec : forall xs ys : pats, { xs = ys } + { xs <> ys }.
+  repeat decide equality.
+  repeat decide equality.
+Defined.
+
+Fixpoint qp p : value :=
+  match p with
+  | pDiscard => vRecord (vSymbol lDiscard) vsNil
+  | pCapture p' => vRecord (vSymbol lCapture) (vs1 (qp p'))
+  | pBool b => vBool b
+  | pSymbol s => vSymbol s
+  | pRecord (pSymbol lDiscard) psNil => vRecord (vQuote (vSymbol lDiscard)) vsNil
+  | pRecord (pSymbol lCapture) (psCons p' psNil) => vRecord (vQuote (vSymbol lCapture)) (vs1 (qp p'))
+  | pRecord (pSymbol lQuote) (psCons p' psNil) => vRecord (vQuote (vSymbol lQuote)) (vs1 (qp p'))
+  | pRecord l ps => vRecord (qp l) (qps ps)
+  | pSeq ps => vSeq (qps ps)
+  end
+with qps ps : values :=
+       match ps with
+       | psNil => vsNil
+       | psCons p' ps' => vsCons (qp p') (qps ps')
+       end.
+
+Fixpoint raw_uqp v : pat :=
+  match v with
+  | vBool b => pBool b
+  | vSymbol s => pSymbol s
+  | vRecord l fs => pRecord (raw_uqp l) (raw_uqps fs)
+  | vSeq vs => pSeq (raw_uqps vs)
+  end
+with raw_uqps vs : pats :=
+       match vs with
+       | vsNil => psNil
+       | vsCons v vs' => psCons (raw_uqp v) (raw_uqps vs')
+       end.
+
+Fixpoint uqp v : pat :=
+  match v with
+  | vRecord (vSymbol lDiscard) vsNil => pDiscard
+  | vRecord (vSymbol lCapture) (vsCons v' vsNil) => pCapture (uqp v')
+  | vRecord (vSymbol lQuote) (vsCons v' vsNil) => raw_uqp v'
+  | vBool b => pBool b
+  | vSymbol s => pSymbol s
+  | vRecord l fs => pRecord (uqp l) (uqps fs)
+  | vSeq vs => pSeq (uqps vs)
+  end
+with uqps vs : pats :=
+       match vs with
+       | vsNil => psNil
+       | vsCons v vs' => psCons (uqp v) (uqps vs')
+       end.
+
+Lemma quoting_for_record_sensible :
+  forall p ps,
+    p <> pSymbol lDiscard ->
+    p <> pSymbol lCapture ->
+    p <> pSymbol lQuote ->
+    uqp (qp (pRecord p ps)) = pRecord (uqp (qp p)) (uqps (qps ps)).
+Proof.
+  destruct p; try reflexivity.
+  destruct l; try congruence; reflexivity.
+  intros; destruct p; try reflexivity.
+  destruct l; try reflexivity; destruct p0; try reflexivity.
+  destruct p0; try reflexivity.
+  destruct p0; try reflexivity.
+Qed.
+
+Theorem quoting_sensible : forall p, uqp (qp p) = p
+with quoting_list_sensible : forall ps, uqps (qps ps) = ps.
+Proof.
+  clear quoting_sensible.
+  induction p; try reflexivity.
+  remember (qp (pCapture p)) as p'; simpl in Heqp'; rewrite Heqp'; simpl; rewrite IHp; reflexivity.
+
+  remember (pat_dec p (pSymbol lDiscard)) as HisDiscard; inversion HisDiscard.
+  remember (pats_dec p0 psNil) as HisEmpty; inversion HisEmpty.
+  rewrite H, H0; reflexivity.
+  rewrite H; remember p0 as p0'; destruct p0'.
+  congruence.
+  simpl.
+  rewrite Heqp0'.
+  rewrite <- quoting_list_sensible with (ps := p0).
+  rewrite <- Heqp0'.
+  reflexivity.
+
+  remember (pat_dec p (pSymbol lCapture)) as HisCapture; inversion HisCapture;
+    [ rewrite H0; clear H0 | ].
+  remember p0 as p0'; destruct p0'; [ reflexivity | ].
+  rewrite Heqp0'.
+  destruct p0';
+    [ simpl | unfold qp];
+    rewrite <- quoting_list_sensible with (ps := p0) at 2;
+    rewrite <- Heqp0';
+    reflexivity.
+
+  remember (pat_dec p (pSymbol lQuote)) as HisQuote; inversion HisQuote;
+    [ rewrite H1; clear H1 | ].
+  remember p0 as p0'; destruct p0'; [ reflexivity | ].
+  rewrite Heqp0'.
+  destruct p0';
+    [ simpl | unfold qp];
+    rewrite <- quoting_list_sensible with (ps := p0) at 2;
+    rewrite <- Heqp0';
+    reflexivity.
+
+  rewrite quoting_for_record_sensible; try assumption.
+  rewrite <- IHp at 2.
+  rewrite <- quoting_list_sensible with (ps := p0) at 2.
+  reflexivity.
+
+  rewrite <- quoting_list_sensible with (ps := p) at 2; reflexivity.
+
+  clear quoting_list_sensible.
+  induction ps; try reflexivity.
+  simpl.
+  rewrite quoting_sensible.
+  f_equal.
+  apply IHps.
+Qed.