\setlength{\parindent}{0pt}
\setlength{\parskip}{1em}

\let\c@mastercounter\relax
\newcounter{mastercounter}[subsection]
\renewcommand\themastercounter{\thesubsection.\arabic{mastercounter}}

\newcommand\pnot{\neg}
\newcommand\por{\vee}
\newcommand\pand{\wedge}
\newcommand\syn{\vdash}
\newcommand\false{\perp}

\newcommand\ass[1]{[#1]}
\newenvironment{logicproof}{%
  \directlua{require("preamble").start_logicproof()}%
}{%
  \directlua{require("preamble").stop_logicproof()}%
}

\newcommand\stypes{{\glsref[stype_symbol]{\Pi}}}
\newcommand\lterms{{\glsref[lterms_symbol]{\Lambda_\Pi}}}
\newcommand\range[1]{\glsref[range_symbol]{|#1|}}
\newcommand\trel{\glsref[trel_symbol]{\Vdash}}
\newcommand\lto{\glsref[lto_symbol]{\lambda(\to)}}
\newcommand\tob{\glsref[tob_symbol]{\to_\beta}}
\newcommand\equivb{\glsref[tob_symbol]{\equiv_\beta}}
\def\subst[#1]{\glsref[subst_symbol]{[#1]}}

\newcommand\tobev{\glsref[tobev_symbol]{\twoheadrightarrow_\beta}}
\newcommand\height{\glsref[h_symbol]{h}}
\newcommand\toe{\glsref[toe_symbol]{\to_\eta}}

\DeclareMathOperator{\case}{case}

\newcommand\himplies{\glsref[himplies_symbol]{\Rightarrow}}
\newcommand\hmodels[1][H]{\glsref[hmodels_symbol]{\models_{#1}}}

\let\interior\relax
\DeclareMathOperator{\interior}{int}

\newcommand\F{\glsref[F_symbol]{F}}
\newcommand\pups{\glsref[pups_symbol]{\uparrow}}
\newcommand\forces{\glsref[forcing_symbol]{\Vdash}}
\newcommand\tsegs{\glsref[tsegs_symbol]{T}}

\newcommand\wforces{\glsref[wforces_symbol]{\Vdash}}

\let\meet\wedge
\let\join\vee

\newcommand\uterms{\glsref[uterms_symbol]{\Lambda}}
\newcommand\tstar[1][]{{\glsref[tstar_symbol]{#1*}}}
\DeclareMathOperator{\FV}{FV}

\newcommand\cn{\glsref[cn_symbol]{c}}

\newcommand\ife[3]{\glsref[ifelse_symbol]{\text{if $#1$ then $#2$ else $#3$}}}
\def\pair[#1, #2]{\glsref[pair_symbol]{[#1, #2]}}
\newcommand\ctop{\glsref[ctopbot_symbol]{\top}}
\newcommand\cbot{\glsref[ctopbot_symbol]{\bot}}
\newcommand\Y{\glsref[fpc]{Y}}

\newcommand\fsucc{\glsref[succ_symbol]{S}}

\newcommand\Gn[1]{\glsref[Gn_symbol]{\left\lceil #1 \right\rceil}}

\let\dom\relax
\DeclareMathOperator{\dom}{dom}

\newcommand\lpa{\glsref[lpa_symbol]{L_{\text{PA}}}}
\DeclareMathOperator{\PAinternal}{PA}
\newcommand\PA{\glsref[lpa_symbol]{\PAinternal}}
\newcommand\delz{\glsref[delz_symbol]{\Delta_0}}
\newcommand\sigone{\glsref[delz_symbol]{\Sigma_1}}
\newcommand\pione{\glsref[delz_symbol]{\Pi_1}}

\newcommand\PAm{\text{\glsref[lpa_symbol]{PA$^{-}$}}}
