Fix rendering of type erasure lemma

macros.tex

@@ -531,10 +531,15 @@
 \newcommand{\Control}{\keyw{control}}
 \newcommand{\Prompt}{\#}
 \newcommand{\Controlz}{\ensuremath{\keyw{control_0}}}
+\newcommand{\Spawn}{\keyw{spawn}}
 \newcommand{\Promptz}{\ensuremath{\#_0}}
 \newcommand{\Escape}{\keyw{escape}}
 \newcommand{\shift}{\keyw{shift}}
 \newcommand{\shiftz}{\ensuremath{\keyw{shift_0}}}
+\newcommand{\CCpp}{\ensuremath{+\CC+}}
+\newcommand{\CCpm}{\ensuremath{+\CC-}}
+\newcommand{\CCmp}{\ensuremath{-\CC+}}
+\newcommand{\CCmm}{\ensuremath{-\CC-}}
 \def\sigh#1{%
 \pmb{\left\langle\vphantom{#1}\right.}%
 #1%

thesis.bib

@@ -3749,4 +3749,15 @@
    editor   = {Andrew M. Pitts and Peter Dybjer},
    pages    = {131--184},
    year     = 1997
-}
+}
+
+# Milner's context lemma
+@article{Milner77,
+  author    = {Robin Milner},
+  title     = {Fully Abstract Models of Typed $\lambda$-Calculi},
+  journal   = {Theor. Comput. Sci.},
+  volume    = {4},
+  number    = {1},
+  pages     = {1--22},
+  year      = {1977}
+}