\usepackage{blindtext}
\usepackage{enumerate}
\usepackage{hyperref, bookmark}
\usepackage{amsmath, amsfonts, amssymb, amsthm}
\usepackage{xcolor}
\usepackage{bussproofs}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
% \newtheorem{prop}[thm]{Proposition}
\newtheorem{corollary}{Corollary}

\theoremstyle{definition}
\newtheorem{definition}{Definition}
% \newtheorem{conj}{Conjecture}[section]
\newtheorem{example}{Example}

% \theoremstyle{remark}
% \newtheorem*{rem}{Remark}
% \newtheorem*{note}{Note}

\newcommand{\defeq}{:=}
\newcommand{\underscore}{\_\!\_}

\newcommand{\TmIdentity}{\operatorname{I}}
\newcommand{\TmTrue}{\operatorname{tt}}
\newcommand{\TmFalse}{\operatorname{ff}}

\newcommand{\SepP}[2]{\langle #1 \mid #2\rangle}
\newcommand{\Subtm}{\preceq}%{\trianglelefteq}
\newcommand{\Subtmapp}{\preceq^a}
\newcommand{\EtaEq}{=_\eta}
\newcommand{\EtaNeq}{\not\EtaEq}
\newcommand{\true}{\operatorname{tt}}
\newcommand{\false}{\operatorname{ff}}
\newcommand{\todo}[1]{{\color{red}#1}}
\newcommand{\ddef}{\mathrel{::=}}
\newcommand{\semi}{\mathrel{;}}

\newcommand{\ih}{\emph{i.h.}}
\newcommand{\ie}{\emph{i.e.}}
\newcommand{\eg}{\emph{e.g.}}
% \newcommand{\EtaNeq}{\mathrel{\texttt{<>}}}

\newcommand{\Commento}[1]{{\bf\color{red}#1}}

\newcommand{\LambdaFire}{$\lambda_f$}
\newcommand{\NewSystem}{$\lambda_{\color{red}???}$}

% explicit substitution objectified
\newcommand{\en}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}
\newcommand{\comma}{\texttt{,}}
\renewcommand{\semi}{\texttt{;}}
\newcommand{\as}{{\ast}} % asterisk

\newcommand{\Operator}[1]{\texttt{#1}}
\newcommand{\Match}[2]{\Operator{match}^{#1}\,#2}
\newcommand{\Branch}[2]{#1\mathrel{\texttt{=>}}#2}
\newcommand{\SepPA}[3]{\langle#1 \mid #2 \mid #3\rangle}
\newcommand{\Sep}{\mathrel{\texttt{|}}}
\newcommand{\Num}{\mathrm{N}}
\newcommand{\Numeral}[1]{\bar{#1}}

\newcommand{\ToFire}[1]{#1{\downarrow}}


% from strong_fireballs macros.tex
\newcommand{\Lam}[1]{\lambda #1.\,}

\newcommand{\hl}[1]{{\underline{#1}}}
\newcommand{\Esub}[2]{\texttt{[}#2\texttt{/}#1\texttt{]}}
\newcommand{\Comma}{\texttt{,}}
\newcommand{\Semi}{\texttt{;}}
\newcommand{\Subst}[2]{\{#2/#1\}}
% \newcommand{\Comma}{}
\newcommand{\tm}{t}
\newcommand{\tmtwo}{u}
\newcommand{\tmthree}{s}
\newcommand{\var}{x}
\newcommand{\vartwo}{y}
\newcommand{\varthree}{z}
\newcommand{\varfour}{w}

\newcommand{\Red}[2]{\xrightarrow{#2}_{#1}}
\newcommand{\TODO}{{\color{red}\textbf{TODO}}}

\renewcommand{\Lam}[2]{\lambda#1.\, \{\!\!\{#2\}\!\!\}}
\renewcommand{\vec}{\overrightarrow}
\newcommand{\reflemma}[1]{Lemma~\ref{l:#1}}