\documentclass{article}
\usepackage{lmodern}%
\usepackage{enumitem}
\usepackage[authoryear]{natbib}

\newtheorem{exercise}{Exercise}[section]
% \newenvironment{exercise}{\begin{@exercise}\rm}{\end{@exercise}}
\newenvironment{ADDITIONAL}[1]{#1}{}
\newenvironment{SOLUTION}[1]{\paragraph*{Solution}\begin{it}#1}{\end{it}}

%\oddsidemargin 0pt
%\evensidemargin \oddsidemargin
%\marginparwidth 0.5in



% \setlength{\topmargin}{15mm}
\setlength{\topmargin}{5mm}

%\setlength{\textwidth}{155mm}
\setlength{\textwidth}{155mm}
%\setlength{\textwidth}{165mm}
\setlength{\textheight}{200mm}
%\setlength{\textheight}{195mm}

\setlength{\evensidemargin}{5mm}
\setlength{\oddsidemargin}{5mm}

\newcommand{\hs}[1]{\hspace{#1}}

% \usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{latexsym}
\usepackage{amsfonts}
\usepackage{listings}
\usepackage{srcltx}
\usepackage{charter}
\usepackage{euler}

\usepackage{latexsym}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{comment}

\ifdefined\studentversion
  \excludecomment{exercise}
  \excludecomment{solution}
  \excludecomment{additional}
\else
% \excludecomment{additional}
\includecomment{exercise}
\includecomment{solution}
\includecomment{additional}
\fi

\newtheorem{@problem}{Exercise}[section]
\newenvironment{problem}{\begin{@problem}\rm}{\end{@problem}}

\newtheorem{@sol}{Solution}[section]
\newenvironment{sol}{\begin{@sol}\rm}{\end{@sol}}

\newcommand{\ext}[1]{\geq_{#1}}

\usepackage{proof}
\usepackage{cdsty}

\newcommand{\nl}{\overline{n}}

\newtheorem{@axiom}{Axiom}
\newenvironment{axiom}{\begin{@axiom}\rm}{\end{@axiom}}
% \newtheorem{@theorem}{Theorem}[section]
% \newenvironment{theorem}{\begin{@theorem}\rm}{\end{@theorem}}

 \newtheorem*{@lemma-nonum}{Lemma}
 \newenvironment{lemma*}{\begin{@lemma-nonum}\rm}{\end{@lemma-nonum}}

 \newtheorem*{@thm-nonum}{Theorem}
 \newenvironment{theorem*}{\begin{@thm-nonum}\rm}{\end{@thm-nonum}}



\input prelude

\usepackage{graphics}
\usepackage{graphicx}

\usepackage{lstextract}

% \includeonly{intro,assign,unif,memo,index,memo-implement,proving}
% \includeonly{index}

\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\G}{\mathcal{G}}
\renewcommand{\H}{\mathcal{H}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\Q}{\mathcal{Q}}

\newcommand{\nf}[2]{#1 : #2 ~\mathsf{nf}}
\newcommand{\neu}[2]{#1 : #2 ~\mathsf{ne}}
\newcommand{\hole}{\mathsf{\_}}
\newcommand{\holetype}{\mathsf{~|~}}


 \newcommand{\one}{1}
\newcommand{\SN}{\mathsf{SN}}
\newcommand{\SNe}{\mathsf{SNe}}
\newcommand{\csn}{\mathsf{sn}}
\newcommand{\CR}{\textsf{CR}}
\newcommand{\denot}[1]{\mathcal{R}_{#1}}
\newcommand{\inden}[3]{#1 \vdash #2 \in \denot{#3}}
\newcommand{\mred}{\longrightarrow^*}
\newcommand{\red}{\longrightarrow}
\newcommand{\redsn}{\longrightarrow_\csn}
\newcommand{\redSN}{\longrightarrow_\SN}
\newcommand{\clos}[1]{\overline{#1}}
\newcommand{\imply}{\Longrightarrow}
\renewcommand{\vec}[1]{\overrightarrow #1}

\newcommand{\id}{\textsf{wk}}
\newcommand{\wk}{\textsf{wk}}

\def\lv{\mathopen{{[\kern-0.14em[}}}    % opening [[ value delimiter
\def\rv{\mathclose{{]\kern-0.14em]}}}   % closing ]] value delimiter
\newcommand{\A}{\mathcal{A}}
% \newcommand{\G}{\mathcal{G}}
\newcommand{\den}[1]{\lv #1 \rv}
\newcommand{\Den}[3][]{\den{#2}^{#1}_{#3}}
\newcommand{\dent}[2]{\llparenthesis#1\rrparenthesis_{#2}}


\long\def\ednote#1{\footnote{[{\it #1\/}]}\message{ednote!}}
% \long\def\note#1{\begin{quote}[{\it #1\/}]\end{quote}\message{note!}}

\begin{document}
\title{POPLMark Reloaded Benchmark: An Introduction \\
-- Work in Progress --}
\author{%
Brigitte Pientka \\ McGill University%
  \and Aliya Hameer \\ McGill University%
  \and Alberto Momigliano \\ University of Milan%
  \and Andreas Abel \\ Chalmers %
%
  }
\date{}
\maketitle

\input{intro.tex}

\input{inductive-defn.tex}

\input{reducibility.tex}

\newpage

\input{extensions.tex}

%\section{Reducibility candidates}
%\section{Forward and backward closed}
%\section{Fundamental lemma}

\bibliographystyle{plainnat}
% \bibliography{../../bibliography/bibi,../../bibliography/bp}
\bibliography{bibi-extract}

\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "sn-proof"
%%% End:

%  LocalWords:  Girard Tait llcl lcl redex subterms iff reducts IH
%  LocalWords:  subst subterm todo Girard's instantiation inl inr
%  LocalWords:  subcases Subcase
