$$
\newcommand{\lolli}{\multimap}
\newcommand{\tensor}{\otimes}
\newcommand{\with}{\&}
\newcommand{\all}[2]{\forall {#1}.\;{#2}}
\newcommand{\fix}[2]{\mu {#1}.\;{#2}}
\newcommand{\letv}[3]{\mathsf{let}\,{#1} = {#2}\;\mathsf{in}\;{#3}}
\newcommand{\Fun}[2]{\Lambda {#1}.\;{#2}}
\newcommand{\fun}[2]{\lambda {#1}.\;{#2}}
\newcommand{\unit}{\left(\right)}
\newcommand{\letunit}[2]{\letv{\unit}{#1}{#2}}
\newcommand{\pair}[2]{\left({#1},{#2}\right)}
\newcommand{\letpair}[4]{\letv{\pair{#1}{#2}}{#3}{#4}}
\newcommand{\unita}{\left[\right]}
\newcommand{\paira}[2]{\left[{#1}, {#2}\right]}
\newcommand{\fst}[1]{\mathsf{fst}\,{#1}}
\newcommand{\snd}[1]{\mathsf{snd}\,{#1}}
\newcommand{\inl}[1]{\mathsf{inl}\,{#1}}
\newcommand{\inr}[1]{\mathsf{inr}\,{#1}}
\newcommand{\case}[5]{\mathsf{case}({#1}, \inl{#2} \to {#3}, \inr{#4} \to {#5})}
\newcommand{\abort}[1]{\mathsf{abort}\,{#1}}
\newcommand{\fold}[1]{\mathsf{in}\,{#1}}
\newcommand{\unfold}[1]{\mathsf{out}\,{#1}}
\newcommand{\judge}[4]{{#1};{#2} \vdash {#3} : {#4}}
\newcommand{\judgetp}[2]{{#1} \ \vdash {#2} : \mathsf{type}}
\newcommand{\judgectx}[2]{{#1} \vdash {#2} : \mathsf{ctx}}
%% Rule names
\newcommand{\rulename}[3]{{#2}{\mathrm{#3}}_{\mathrm{#1}}}
\newcommand{\intro}[2][]{\rulename{#1}{#2}{I}}
\newcommand{\elim}[2][]{\rulename{#1}{#2}{E}}
\newcommand{\Var}{\rulename{}{}{Var}}
\newcommand{\AllI}{\intro{\forall}}
\newcommand{\AllE}{\elim{\forall}}
\newcommand{\LolliI}{\intro{\lolli}}
\newcommand{\LolliE}{\elim{\lolli}}
\newcommand{\UnitI}{\intro{1}}
\newcommand{\UnitE}{\elim{1}}
\newcommand{\TensorI}{\intro{\tensor}}
\newcommand{\TensorE}{\elim{\tensor}}
\newcommand{\TopI}{\intro{\top}}
\newcommand{\TopE}{\elim{\top}}
\newcommand{\WithI}{\intro{\with}}
\newcommand{\WithEFst}{\elim[fst]{\with}}
\newcommand{\WithESnd}{\elim[snd]{\with}}
\newcommand{\ZeroI}{\intro{0}}
\newcommand{\ZeroE}{\elim{0}}
\newcommand{\SumIInl}{\intro[inl]{\oplus}}
\newcommand{\SumIInr}{\intro[inr]{\oplus}}
\newcommand{\SumE}{\elim{\oplus}}
\newcommand{\MuI}{\intro{\mu}}
\newcommand{\MuE}{\elim{\mu}}
\newcommand{\size}[1]{\left|#1\right|}
\newcommand{\inferrule}[3][]{\frac{#2}{#3}\;{#1}}
\newcommand{\tsf}[1]{\textsf{#1}}
\newcommand{\ttt}[1]{\texttt{#1}}
\newcommand{\qamp}{&\quad}
\newcommand{\qqamp}{&&\quad}
\newcommand{\proves}{\vdash}
\newcommand{\hasType}[2]{#1 : #2}
\newcommand{\typeJ}[3]{#1 \proves \hasType{#2}{#3}}
\newcommand{\ctx}{\Gamma}
\newcommand{\typeJC}[2]{\typeJ{\ctx}{#1}{#2}}
\newcommand{\val}[1]{#1~\textsf{val}}
\newcommand{\error}[1]{#1~\textsf{error}}
\newcommand{\num}[1]{\texttt{Int}(#1)}
\newcommand{\steps}[2]{#1 \mapsto #2}
\newcommand{\subst}[3]{[#1 \rightarrow #2] \ #3}
\newcommand{\err}[1]{#1~\textsf{err}}
\newcommand{\lett}[4]{\ttt{let} \ \hasType{#1}{#2} = #3 \ \ttt{in} \ #4}
\newcommand{\rec}[3]{\ttt{rec}(#1; x.y.#2)(#3)}
\newcommand{\s}{\hspace{1em}}
\newcommand{\nl}{\\[2em]}
\newcommand{\ir}[3]{\inferrule[\text{(#1)}]{#2}{#3}}
\newcommand{\Coloneqq}{::=}
\newcommand{\trans}[2]{#1 \leadsto #2}
\newcommand{\app}[2]{#1 \ #2}
\newcommand{\fnt}[3]{\ttt{fn} \ (\hasType{#1}{#2}) \ . \ #3}
\newcommand{\lett}[3]{\ttt{let} \ #1 = #2 \ \ttt{in} \ #3}
\newcommand{\tint}{\ttt{int}}
$$