diff --git a/jfp-paper/defs.tex b/jfp-paper/defs.tex
new file mode 100644
index 0000000000000000000000000000000000000000..647998feedc3d8e758c60ff288697da40464e78f
--- /dev/null
+++ b/jfp-paper/defs.tex
@@ -0,0 +1,172 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% WARNING: I changed these commands
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\renewcommand{\u}{\underline}
+\renewcommand{\sup}[2]{\srho{\upcast{#1}{#2}}}
+
+%% This is a proof that only appears in the long version, and is
+%% otherwise completely omitted
+\NewEnviron{longproof}{%
+  \iflong\begin{proof}\BODY \end{proof}\fi%
+}
+\NewEnviron{longfigure}{%
+  \iflong\begin{figure}\BODY \end{figure}\fi%
+}
+\NewEnviron{longonly}{%
+  \iflong\BODY \fi%
+}
+\NewEnviron{shortonly}{%
+  \ifshort\BODY \fi%
+}
+
+%% \newtheorem*{nonnum-theorem}{Theorem}
+
+\newcommand{\cbpv}{CBPV}
+\newcommand{\cbpvstar}{CBPV*}
+\newcommand{\cbpvtxt}{\cbpv}
+\newcommand{\sem}[1]{\llbracket#1\rrbracket}
+\newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
+\newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
+\newcommand{\srho}[1]{\sem{#1}_\rho}
+\newcommand{\sdn}[2]{\srho{\dncast{#1}{#2}}}
+\newcommand{\hetplug}[1]{\langle#1\rangle}
+\newcommand{\nats}{\mathbb{N}}
+\newtheorem{principle}{Principle}
+\newcommand{\vtype}{\,\,\text{val type}}
+\newcommand{\ctype}{\,\,\text{comp type}}
+\newcommand{\ctx}{\,\,\text{ctx}}
+\newcommand{\stoup}{\,\,\text{stoup}}
+\newcommand{\pipe}{\,\,|\,\,}
+\newcommand{\hole}{\bullet}
+\newcommand{\floor}[1]{\lfloor#1\rfloor}
+\newcommand{\ltdyn}{\sqsubseteq}
+\newcommand{\gtdyn}{\sqsupseteq}
+
+\newcommand{\precltdyn}{\mathrel{\preceq\ltdyn}}
+\newcommand{\precgtdyn}{\mathrel{\preceq\gtdyn}}
+\newcommand{\ltdynsucc}{\mathrel{\ltdyn\succeq}}
+\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
+\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
+\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
+\newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
+\newcommand{\logpole}{\mathrel{\lesssim^{log}_{\pole}}}
+\newcommand{\pole}{\Bot}
+\newcommand{\ipole}[1]{\mathrel{\pole^{#1}}}
+\newcommand{\logc}[1]{\mathrel{\pole}^{#1}}
+\newcommand{\logty}[2]{\mathrel{\lesssim^{#1}_{#2,\pole}}}
+\newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
+\newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}}
+\newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}}
+\newcommand{\ltlog}{\mathrel{\ltdyn^{log}}}
+
+\newcommand{\apreorder}{\trianglelefteq}
+\newcommand{\ctxpreorder}{\mathrel{\apreorder^{\text{ctx}}}}
+\newcommand{\ctxize}[1]{\mathrel{{#1}^{\text{ctx}}}}
+\newcommand{\ix}[2]{\mathrel{#1^{#2}}}
+\newcommand{\simsub}[1]{\mathrel{\sim_{#1}}}
+
+\newcommand{\itylrof}[3]{\ilrof{#1}{#3,#2}}
+\newcommand{\ilrof}[2]{\mathrel{{#1}^{\text{log}}_{#2}}}
+\newcommand{\itylr}[2]{\itylrof{\apreorder}{#1}{#2}}
+\newcommand{\ilr}[1]{\ilrof{\apreorder}{#1}}
+
+\newcommand{\simp}[1]{{#1}^{\dag}}
+\newcommand{\simpp}[1]{\simp{({#1})}}
+
+%% Operational steps
+\newcommand{\step}{\mapsto}
+\newcommand{\stepsin}[1]{\mathrel{\mapsto^{#1}}}
+\newcommand{\stepzero}{\stepsin 0}
+\newcommand{\stepone}{\stepsin 1}
+\newcommand{\stepstar}{\stepsin{*}}
+\newcommand{\bigstepsin}[1]{\mathrel{\Mapsto^{#1}}}
+\newcommand{\bigstepzero}{\bigstepsin{0}}
+\newcommand{\bigstepany}{\bigstepsin{}}
+
+\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
+\newcommand{\pairone}[1]{\{ \pi \mapsto {#1}}
+\newcommand{\pairtwo}[1]{\pipe \pi' \mapsto {#1}\}}
+\newcommand{\emptypair}[0]{\{\}}
+\newcommand{\pairWtoXYtoZ}[4]{\{ #1 \mapsto {#2} \pipe #3 \mapsto {#4}\}}
+\newcommand{\tru}{\texttt{true}}
+\newcommand{\fls}{\texttt{false}}
+\newcommand{\ifXthenYelseZ}[3]{\kw{if}#1\,\kw{then}#2\,\kw{else}#3}
+\newcommand{\bool}{\mathbb{B}}
+\newcommand{\inl}{\kw{inl}}
+\newcommand{\inr}{\kw{inr}}
+\newcommand{\intag}[1]{\texttt{in}_{#1}}
+\newcommand{\els}{\kw {else}}
+\newcommand{\seq}{\texttt{seq}}
+
+\newcommand{\dyn}{{?}}
+\newcommand{\dynv}{{?}}
+\newcommand{\dync}{\u {\text{?`}}}
+\newcommand{\uarrow}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
+\newcommand{\darrow}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
+\newcommand{\upcast}[2]{\langle{#2}\uarrow{#1}\rangle}
+\newcommand{\dncast}[2]{\langle{#1}\darrow{#2}\rangle}
+\newcommand{\obcast}[2]{\langle{#1}\Leftarrow{#2}\rangle}
+\newcommand{\err}{\mho}
+\newcommand{\diverge}{\Omega}
+\newcommand{\print}{\kw{print}}
+\newcommand{\roll}{\kw{roll}}
+\newcommand{\rollty}[1]{\texttt{roll}_{#1}\,\,}
+\newcommand{\unroll}{\kw{unroll}}
+\newcommand{\unrollty}[1]{\texttt{unroll}_{#1}\,\,}
+\newcommand{\defupcast}[2]{\langle\kern-1ex~\langle{#2}\uarrow{#1}\rangle\kern-1ex~\rangle}
+\newcommand{\defdncast}[2]{\langle\kern-1ex~\langle{#1}\darrow{#2}\rangle\kern-1ex~\rangle}
+
+\newcommand{\result}{\text{result}}
+\newcommand{\Set}{\text{Set}}
+\newcommand{\relto}{\to}
+\newcommand{\M}{\mathcal{M}}
+\newcommand{\sq}{\square}
+\newcommand{\lett}{\kw{let}}
+\newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
+\newcommand{\bindXtoYinZ}[2]{\kw{bind}#2 \leftarrow #1;}
+\newcommand{\too}{\kw{to}}
+\newcommand{\case}{\kw{case}}
+\newcommand{\kw}[1]{\texttt{#1}\,\,}
+\newcommand{\absurd}{\kw{absurd}}
+\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
+\newcommand{\caseofX}[1]{\case #1}
+\newcommand{\thenY}{\{}
+\newcommand{\elseZ}[1]{\pipe #1 \}}
+\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
+\newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
+\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
+\newcommand{\ret}{\kw{ret}}
+\newcommand{\thunk}{\kw{thunk}}
+\newcommand{\force}{\kw{force}}
+\newcommand{\abort}{\kw {abort}}
+\newcommand{\with}{\mathbin{\&}}
+
+\newcommand{\dyncaseofXthenOnePairSumU}[5]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \pipe #5 \}}
+\newcommand{\dyncaseofXthenYelseZ}[3]{\kw{tycase} #1\,\{ #2 \pipe #3 \}}
+\newcommand{\dyncocaseWithFunF}[3]{\{\with \mapsto #1 \pipe (\to) \mapsto #2 \pipe \u F \mapsto #3 \}}
+\newcommand{\dyncaseofXthenBoolUPair}[4]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \}}
+\newcommand{\dyncocaseFunF}[2]{\{(\to) \mapsto #1 \pipe \u F \mapsto #2 \}}
+
+\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
+\newcommand{\alt}{\bnfalt}
+\newcommand{\bnfdef}{\mathrel{\bf ::=}}
+\newcommand{\bnfadd}{\mathrel{\bf +::=}}
+\newcommand{\bnfsub}{\mathrel{\bf -::=}}
+
+\newcommand\dynvctx[0]{\mathsf{dyn\mathord{-}vctx}}
+\newcommand\dyncctx[0]{\mathsf{dyn\mathord{-}cctx}}
+
+\newcommand\leastdynv[0]{\bot_{\mathsf{v}}}
+\newcommand\leastdync[0]{\bot_{\mathsf{c}}}
+
+\newcommand\errordivergeleft[0]{\preceq\ltdyn}
+\newcommand\errordivergeright[0]{\ltdyn\succeq}
+\newcommand\errordivergerightop[0]{\preceq\gtdyn}
+
+\newcommand\bvtopv[1]{#1^{c}}
+\newcommand\bvtopvpure[1]{#1^{v}}
+\newcommand\purely{\downarrow}
+
+%% Local Variables:
+%% compile-command: "./latexrun jfp-gtt.tex"
+%% End: