+\usepackage{blindtext}\r
+\usepackage{enumerate}\r
+\usepackage{hyperref, bookmark}\r
+\usepackage{amsmath, amsfonts, amssymb, amsthm}\r
+\usepackage{xcolor}\r
\usepackage{bussproofs}\r
\r
\theoremstyle{plain}\r
\newtheorem{theorem}{Theorem}\r
\newtheorem{lemma}{Lemma}\r
% \newtheorem{prop}[thm]{Proposition}\r
-% \newtheorem*{cor}{Corollary}\r
+\newtheorem{corollary}{Corollary}\r
\r
\theoremstyle{definition}\r
\newtheorem{definition}{Definition}\r
\newcommand{\Numeral}[1]{\bar{#1}}\r
\r
\newcommand{\ToFire}[1]{#1{\downarrow}}\r
+\r
+\r
+% from strong_fireballs macros.tex\r
+\newcommand{\Lam}[1]{\lambda #1.\,}\r
+\r
+\newcommand{\hl}[1]{{\underline{#1}}}\r
+\newcommand{\Esub}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}\r
+\newcommand{\Comma}{\texttt{,}}\r
+\newcommand{\Semi}{\texttt{;}}\r
+\newcommand{\Subst}[2]{\{#2/#1\}}\r
+% \newcommand{\Comma}{}\r
+\newcommand{\tm}{t}\r
+\newcommand{\tmtwo}{u}\r
+\newcommand{\tmthree}{s}\r
+\newcommand{\var}{x}\r
+\newcommand{\vartwo}{y}\r
+\newcommand{\varthree}{z}\r
+\newcommand{\varfour}{w}\r
+\r
+\newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}\r
+\newcommand{\TODO}{{\color{red}\textbf{TODO}}}\r
+\r
+\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}\r
+\renewcommand{\vec}{\overrightarrow}\r
+\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}\r
+\newcommand{\head}{h}\r
+\newcommand{\args}{a}\r