\newcommand{\typing}[3][\Gamma]{#1 \vdash #2 : #3}
\newcommand{\llbracket}{\textlbrackdbl}
\newcommand{\rrbracket}{\textrbrackdbl}
\newcommand{\oxford}[1]{\llbracket #1\rrbracket}
\newcommand{\denotes}[2][v]{\oxford{#2}#1}
\newcommand{\compile}[1]{\lfloor #1\rfloor}
\newcommand{\lift}[1]{\lceil #1\rceil}
\newcommand{\encrypt}[2]{\{#1\}_{#2}}
\newcommand{\sign}[2]{\{\!|#1|\!\}_{#2}}
\newcommand{\hash}[1]{|#1|}
\newcommand{\evalop}{\rightarrow}
\newcommand{\evalopm}{\rightarrow^*}
\newcommand{\eval}{\;\evalop\;}
\newcommand{\evals}[2]{#1\evalop #2}
\newcommand{\evalm}[2]{#1\evalopm #2}
\newcommand{\succ}{\mathsf{succ}\;}
\newcommand{\pred}{\mathsf{pred}\;}
\newcommand{\iszero}{\mathsf{isZero}\;}
\newcommand{\ifte}[3]{(\mathsf{if}\ #1\ #2\ #3)}
\newcommand{\tru}{\mathsf{true}}
\newcommand{\fls}{\mathsf{false}}
\newcommand{\Unit}{\mathsf{Unit}}
\newcommand{\unit}{\mathsf{unit}}
\newcommand{\let}[3]{\mathsf{let}\; #1 = #2\;\mathsf{in}\;#3}
\newcommand{\letrec}[3]{\mathsf{letrec}\; #1 = #2\;\mathsf{in}\;#3}
\newcommand{\RLS}[1]{\RL{\quad\textsf{#1}}}