diff --git a/quoting.v b/quoting.v
index b2976f1..1c8390c 100644
--- a/quoting.v
+++ b/quoting.v
@@ -1,5 +1,6 @@
 Require Import Coq.Lists.List.
-Require Import String.
+Require Import Coq.Strings.String.
+Require Import Coq.Program.Equality.
 Import ListNotations.
 Open Scope list_scope.
 Open Scope string_scope.
@@ -26,46 +27,21 @@ Inductive pat : Type :=
 
 Definition vQuote v : value := vRecord (vSymbol lQuote) [v].
 
-Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
-  repeat decide equality.
+Fixpoint value_ind'
+         (P : value -> Prop)
+         (PBool : forall b, P (vBool b))
+         (PSymbol : forall l, P (vSymbol l))
+         (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.
 
-Fixpoint pat_dec (x y : pat) : { x = y } + { x <> y }.
-  repeat decide equality.
-Defined.
-
-Fixpoint qp p : value :=
-  match p with
-  | pDiscard => vRecord (vSymbol lDiscard) []
-  | pCapture p' => vRecord (vSymbol lCapture) [qp p']
-  | pBool b => vBool b
-  | pSymbol s => vSymbol s
-  | pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
-  | pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [qp p']
-  | pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [qp p']
-  | pRecord l ps => vRecord (qp l) (map qp ps)
-  | pSeq ps => vSeq (map qp 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) (map raw_uqp fs)
-  | vSeq vs => pSeq (map raw_uqp vs)
-  end.
-
-Fixpoint uqp v : pat :=
-  match v with
-  | vRecord (vSymbol lDiscard) [] => pDiscard
-  | vRecord (vSymbol lCapture) [v'] => pCapture (uqp v')
-  | vRecord (vSymbol lQuote) [v'] => raw_uqp v'
-  | vBool b => pBool b
-  | vSymbol s => pSymbol s
-  | vRecord l fs => pRecord (uqp l) (map uqp fs)
-  | vSeq vs => pSeq (map uqp vs)
-  end.
-
 Fixpoint pat_ind'
          (P : pat -> Prop)
          (PDiscard : P pDiscard)
@@ -83,8 +59,68 @@ Proof.
                 apply IHl ].
 Defined.
 
-Lemma Forall_map_map_id : forall ps, Forall (fun p : pat => uqp (qp p) = p) ps ->
-                                     (map uqp (map qp ps)) = ps.
+Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
+  repeat decide equality.
+Defined.
+
+Fixpoint pat_dec (x y : pat) : { x = y } + { x <> y }.
+  repeat decide equality.
+Defined.
+
+Scheme Equality for label.
+
+Fixpoint mat p v : bool :=
+  let matseq := (fix matseq ps vs : bool :=
+                   match ps, vs with
+                   | [], [] => true
+                   | (p :: ps'), (v :: vs') => andb (mat p v) (matseq ps' vs')
+                   | _, _ => false
+                   end) in
+  match p with
+  | pDiscard => true
+  | pCapture p' => mat p' v
+  | pBool b => match v with vBool b' => bool_beq b b' | _ => false end
+  | pSymbol s => match v with vSymbol s' => label_beq s s' | _ => false end
+  | pRecord p' ps => match v with vRecord v' vs => mat p' v' && matseq ps vs | _ => false end
+  | pSeq ps => match v with vSeq vs => matseq ps vs | _ => false end
+  end.
+
+Fixpoint raw_v_to_p v : pat :=
+  match v with
+  | vBool b => pBool b
+  | vSymbol s => pSymbol s
+  | vRecord l fs => pRecord (raw_v_to_p l) (map raw_v_to_p fs)
+  | vSeq vs => pSeq (map raw_v_to_p vs)
+  end.
+
+Fixpoint v_to_p v : pat :=
+  match v with
+  | vRecord (vSymbol lDiscard) [] => pDiscard
+  | vRecord (vSymbol lCapture) [v'] => pCapture (v_to_p v')
+  | vRecord (vSymbol lQuote) [v'] => raw_v_to_p v'
+  | vBool b => pBool b
+  | vSymbol s => pSymbol s
+  | vRecord l fs => pRecord (v_to_p l) (map v_to_p fs)
+  | vSeq vs => pSeq (map v_to_p vs)
+  end.
+
+Fixpoint p_to_v p : value :=
+  match p with
+  | pDiscard => vRecord (vSymbol lDiscard) []
+  | pCapture p' => vRecord (vSymbol lCapture) [p_to_v p']
+  | pBool b => vBool b
+  | pSymbol s => vSymbol s
+  | pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
+  | pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [p_to_v p']
+  | pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [p_to_v p']
+  | pRecord l ps => vRecord (p_to_v l) (map p_to_v ps)
+  | pSeq ps => vSeq (map p_to_v ps)
+  end.
+
+Lemma Forall_map_map_id :
+  forall A X xs (f : X -> A) (g : A -> X),
+    Forall (fun x : X => g (f x) = x) xs ->
+    (map g (map f xs)) = xs.
 Proof.
   intros; rewrite map_map; induction H; [ reflexivity | ].
   simpl; rewrite IHForall; rewrite H; reflexivity.
@@ -92,27 +128,246 @@ Qed.
 
 Ltac solve_map_map_id := repeat f_equal; apply Forall_map_map_id; assumption.
 
-Theorem quoting_sensible : forall p, uqp (qp p) = p.
+Theorem reflection_after_interpretation_sensible : forall p, v_to_p (p_to_v p) = p.
 Proof.
   induction p using pat_ind';
     try solve [ reflexivity
               | rewrite <- IHp at 2; reflexivity
               | simpl; solve_map_map_id ].
-
   destruct p; simpl; try rewrite <- IHp; try solve [ solve_map_map_id ].
 
   (* label pSymbol *)
+
   destruct l;
-    [ destruct ps; [ reflexivity | inversion H; simpl; rewrite H2; solve_map_map_id ]
-    | | | simpl; solve_map_map_id ];
-    try solve [ destruct ps; [ reflexivity | ];
-      destruct ps; [ inversion H; simpl; rewrite H2; reflexivity | ];
-      inversion H; simpl; rewrite H2;
-      inversion H3; simpl; rewrite H6;
-      solve_map_map_id ].
+    apply Forall_map_map_id in H;
+    destruct ps; simpl in H; inversion H; clear H; auto;
+      destruct ps; simpl; repeat f_equal;
+        try solve [ repeat rewrite H1; reflexivity
+                  | inversion H2; repeat rewrite H0; repeat rewrite H3; reflexivity ].
 
   (* label pRecord *)
   destruct p; try solve_map_map_id;
     destruct l0; destruct l; try solve_map_map_id;
       destruct l; solve_map_map_id.
 Qed.
+
+Theorem interpretation_after_reflection_not_sensible :
+  exists v, p_to_v (v_to_p v) <> v.
+Proof.
+  exists (vQuote (vRecord (vSymbol lDiscard) [])).
+  simpl; intro H; inversion H.
+Qed.
+
+Fixpoint escape v : value :=
+  match v with
+  | vBool b => vBool b
+  | vSymbol s => vSymbol s
+  | vRecord (vSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
+  | vRecord (vSymbol lCapture) [v'] => vRecord (vQuote (vSymbol lCapture)) [escape v']
+  | vRecord (vSymbol lQuote) [v'] => vRecord (vQuote (vSymbol lQuote)) [escape v']
+  | vRecord l vs => vRecord (escape l) (map escape vs)
+  | vSeq vs => vSeq (map escape vs)
+  end.
+
+Fixpoint unescape v : value :=
+  match v with
+  | vBool b => vBool b
+  | vSymbol s => vSymbol s
+  | vRecord (vSymbol lQuote) [v'] => v'
+  | vRecord l vs => vRecord (unescape l) (map unescape vs)
+  | vSeq vs => vSeq (map unescape vs)
+  end.
+
+Theorem unescape_after_escape_id : forall v, unescape (escape v) = v.
+Proof.
+  induction v using value_ind'; auto.
+
+  destruct v; simpl; try rewrite <- IHv; try solve [ solve_map_map_id ].
+
+  (* vRecord with a vSymbol label *)
+
+  destruct l;
+    apply Forall_map_map_id in H;
+    destruct vs; simpl in H; inversion H; clear H; auto;
+      destruct vs; simpl; repeat f_equal;
+        try solve [ repeat rewrite H1; reflexivity
+                  | inversion H2; repeat rewrite H0; repeat rewrite H3; reflexivity ].
+
+  (* vRecord with a vRecord label *)
+
+  destruct v; try solve_map_map_id;
+    destruct l0; destruct l; try solve_map_map_id;
+      destruct l; solve_map_map_id.
+
+  (* vSeq *)
+
+  destruct vs; inversion H; clear H;
+    simpl; repeat rewrite H2; repeat rewrite H3; solve_map_map_id.
+Qed.
+
+Lemma Forall_map_map_assoc_id :
+  forall A X Y ys (h : Y -> X) (f : X -> A) (g : A -> X),
+    Forall (fun y : Y => g (f (h y)) = (h y)) ys ->
+    map g (map f (map h ys)) = (map h ys).
+Proof.
+  intros; rewrite map_map; induction H; [ reflexivity | ].
+  simpl; rewrite IHForall; rewrite H; reflexivity.
+Qed.
+
+Ltac solve_map_map_assoc_id := repeat f_equal; apply Forall_map_map_assoc_id; assumption.
+
+Lemma escape_record_record_label :
+  forall l inner outer,
+    escape (vRecord (vRecord l inner) outer) = vRecord (escape (vRecord l inner)) (map escape outer).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma Forall_map_map_raw :
+  forall B A X xs (h : X -> A) (f : X -> B) (g : B -> A),
+    Forall (fun x : X => (g (f x)) = (h x)) xs ->
+    map g (map f xs) = (map h xs).
+Proof.
+  intros; rewrite map_map; induction H; [ reflexivity | ].
+  simpl; rewrite IHForall; rewrite H; reflexivity.
+Qed.
+
+Lemma escaped_record_is_record :
+  forall v l, exists l' v', escape (vRecord v l) = vRecord v' l'.
+Proof.
+  intros.
+  exists (map escape l).
+  remember v as x.
+  induction x using value_ind'; try destruct l0; try destruct l; try destruct l;
+    try solve [ exists v; subst; reflexivity
+              | exists (vQuote (vSymbol lDiscard)); reflexivity
+              | exists (vQuote (vSymbol lCapture)); reflexivity
+              | exists (vQuote (vSymbol lQuote)); reflexivity
+              | exists (escape (vRecord x vs)); reflexivity
+              | exists (escape (vSeq vs)); reflexivity ].
+Qed.
+
+Lemma v_to_p_escaped_record_is_raw_v_to_p :
+  forall v, v_to_p (escape v) = (raw_v_to_p v).
+Proof.
+  induction v using value_ind'; try reflexivity.
+
+  destruct v.
+
+  simpl; rewrite Forall_map_map_raw with (h := raw_v_to_p); auto.
+
+  destruct l; destruct vs; simpl; inversion IHv; try reflexivity;
+    (destruct vs; simpl; inversion H; rewrite H2; try reflexivity;
+     inversion H3; rewrite H6;
+     rewrite Forall_map_map_raw with (h := raw_v_to_p); auto).
+
+  unfold raw_v_to_p; fold raw_v_to_p;
+    (replace (pRecord (raw_v_to_p v) (map raw_v_to_p l)) with (raw_v_to_p (vRecord v l));
+     [ | reflexivity ]);
+    rewrite <- IHv;
+    rewrite escape_record_record_label;
+    (assert (exists (l' : list value) (v' : value), escape (vRecord v l) = vRecord v' l');
+     [ apply escaped_record_is_record | ]);
+    inversion_clear H0; inversion_clear H1;
+      rewrite H0; rewrite <- Forall_map_map_raw with (f := escape) (g := v_to_p); auto.
+
+  simpl; f_equal; [ apply IHv | ]; apply Forall_map_map_raw; assumption.
+
+  simpl; f_equal; apply Forall_map_map_raw; assumption.
+Qed.
+
+Lemma p_to_v_of_raw_v_to_p_is_escape :
+  forall v,
+    p_to_v (raw_v_to_p v) = escape v.
+Proof.
+  induction v using value_ind'; try reflexivity.
+
+  dependent induction v.
+    (* unfold raw_v_to_p; fold raw_v_to_p; *)
+    (*   unfold p_to_v; fold p_to_v. *)
+
+  simpl; f_equal; f_equal; apply Forall_map_map_raw; assumption.
+
+  destruct l; destruct vs; simpl; inversion IHv; try reflexivity;
+    (destruct vs; simpl; inversion H; rewrite H2; try reflexivity;
+     inversion H3; rewrite H6;
+     rewrite Forall_map_map_raw with (h := escape); [ | assumption ]; reflexivity).
+
+  destruct v; simpl; inversion IHv0; f_equal; f_equal;
+    try solve [ apply Forall_map_map_raw; assumption ].
+
+  simpl; inversion IHv;
+    rewrite <- Forall_map_map_raw with (f := raw_v_to_p) (g := p_to_v); [ | assumption ]; reflexivity.
+
+  inversion H; try reflexivity;
+    simpl; rewrite H0;
+      rewrite <- Forall_map_map_raw with (f := raw_v_to_p) (g := p_to_v); [ | assumption ]; reflexivity.
+Qed.
+
+Lemma interpretation_after_reflection_after_escape_sensible v : p_to_v (v_to_p (escape v)) = (escape v).
+Proof.
+  rewrite v_to_p_escaped_record_is_raw_v_to_p.
+  apply p_to_v_of_raw_v_to_p_is_escape.
+Qed.
+
+Theorem unescape_interpretation_reflection_escape_sensible v : unescape (p_to_v (v_to_p (escape v))) = v.
+Proof.
+  rewrite interpretation_after_reflection_after_escape_sensible.
+  apply unescape_after_escape_id.
+Qed.
+
+Fixpoint quotation_invariant v u : mat (v_to_p (escape v)) u = true <-> u = v.
+Proof.
+  destruct v;
+    destruct u;
+    rewrite v_to_p_escaped_record_is_raw_v_to_p;
+    (split; intro Hlhs; [ | rewrite Hlhs ]);
+    try solve [ simpl in * |- *; congruence ].
+
+  apply internal_bool_dec_bl in Hlhs; congruence.
+  apply internal_bool_dec_lb; reflexivity.
+
+  apply internal_label_dec_bl in Hlhs; congruence.
+  apply internal_label_dec_lb; reflexivity.
+
+  simpl in Hlhs; symmetry in Hlhs; apply Bool.andb_true_eq in Hlhs; inversion_clear Hlhs.
+  symmetry in H, H0.
+  rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
+  rewrite quotation_invariant in H.
+  subst u; f_equal.
+  dependent induction l; dependent induction l0;
+    try solve [ reflexivity
+              | simpl in H0; congruence ].
+  simpl in H0.
+  simpl in H0; symmetry in H0; apply Bool.andb_true_eq in H0; inversion_clear H0.
+  symmetry in H, H1.
+  rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
+  rewrite quotation_invariant in H.
+  subst a0; f_equal.
+  apply IHl.
+  assumption.
+
+  simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
+  rewrite quotation_invariant; reflexivity.
+  clear Hlhs; induction l; [ reflexivity | ].
+  simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
+  rewrite quotation_invariant; reflexivity.
+  apply IHl.
+
+  dependent induction l; dependent induction l0;
+    try solve [ reflexivity
+              | simpl in Hlhs; congruence ].
+  simpl in Hlhs.
+  simpl in Hlhs; symmetry in Hlhs; apply Bool.andb_true_eq in Hlhs; inversion_clear Hlhs.
+  symmetry in H, H0.
+  rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
+  rewrite quotation_invariant in H.
+  subst a0; f_equal.
+  apply IHl in H0.
+  congruence.
+
+  clear Hlhs; induction l; [ reflexivity | ].
+  simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
+  rewrite quotation_invariant; reflexivity.
+  apply IHl.
+Qed.