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

\renewcommand\eslink{http://www.dpmms.cam.ac.uk/study/II/Logic/}

{
\makeatletter
\@addtoreset{customlemma}{section}
\makeatother
\renewtheorem{customlemma}{Lemma}
\renewtheorem{customtheorem}[customlemma]{Theorem}
\renewtheorem{customproposition}[customlemma]{Proposition}
\renewtheorem{customcorollary}[customlemma]{Corollary}
\renewtheorem{customdefinition}[customlemma]{Definition}
\renewtheorem{customexample}[customlemma]{Example}
\renewtheorem{customremark}[customlemma]{Remark}
}

\newcommand\impl{\Rightarrow}

\newcommand\false{\glshyperlink[\perp]{false_notation}}
\newcommand\propL{\glshyperlink[L]{propL_notation}}
\newcommand\propLnum[1]{\glshyperlink[L_{#1}]{propLnum_notation}}
\newcommand\propP{\glshyperlink[P]{propP_notation}}

\newcommand\pand{\glshyperlink[\wedge]{and_notation}}
\newcommand\por{\glshyperlink[\vee]{or_notation}}
\newcommand\true{\glshyperlink[\top]{true_notation}}
\newcommand\pnot{\glshyperlink[\neg]{not_notation}}
\newcommand\propv{\glshyperlink[v]{propv_notation}}

\newcommand\sementails{\glshyperlink[\models]{pentails_notation}}
\newcommand\taut{\glshyperlink[\models]{ptaut_notation}}
\newcommand\synentails{\glshyperlink[\vdash]{psynentails_notation}}
\newcommand\ptheorem{\glshyperlink[\vdash]{ptheorem_notation}}

\newcommand\llt{\glshyperlink[<]{linord_notation}}
\newcommand\lgt{\glshyperlink[>]{leetc_notation}}
\newcommand\lle{\glshyperlink[\le]{leetc_notation}}
\newcommand\lge{\glshyperlink[\ge]{leetc_notation}}
\newcommand\wlt{\glshyperlink[<]{wellord_notation}}
\newcommand\wgt{\glshyperlink[>]{wellord_notation}}
\newcommand\wle{\glshyperlink[\le]{wellord_notation}}
\newcommand\wge{\glshyperlink[\ge]{wellord_notation}}
\newcommand\I{\glshyperlink[I]{Ix_notation}}

\DeclareMathOperator{\dom}{dom}
\newcommand\wole{\glshyperlink[\le]{wole_notation}}
\newcommand\woge{\glshyperlink[\ge]{wole_notation}}

\newcommand\wolt{\glshyperlink[<]{wolt_notation}}
\newcommand\wogt{\glshyperlink[>]{wolt_notation}}
\newcommand\wsucc{\glshyperlink[{}^+]{succ_notation}}
\newcommand\osucc{\glshyperlink[{}^+]{osucc_notation}}
\newcommand\ole{\glshyperlink[\le]{ole_notation}}
\newcommand\olt{\glshyperlink[<]{olt_notation}}
\newcommand\oge{\glshyperlink[\ge]{olt_notation}}
\newcommand\ogt{\glshyperlink[>]{olt_notation}}
\DeclareMathOperator{\OTinternal}{OT}
\newcommand\OT{\glshyperlink[\OTinternal]{ot}}
\newcommand\oI{\glshyperlink[I]{oI_notation}}
\newcommand\oomega{{\glshyperlink[\omega]{oomega_notation}}}

\newcommand\omegaone{\glshyperlink[\omega_1]{omegaone_notation}}
\newcommand\opl{\glshyperlink[+]{opl_notation}}

\newcommand\sopl{\glshyperlink[+]{sopl_notation}}
\newcommand\wocup{\glshyperlink[\sqcup]{wocup_notation}}
\newcommand\ocdot{\glshyperlink[\cdot]{ocdot_notation}}
\newcommand\socdot{\glshyperlink[\cdot]{ocdot_notation}}
\newcommand\ple{\glshyperlink[\le]{ple_notation}}
\newcommand\plt{\glshyperlink[<]{ple_notation}}
\newcommand\pge{\glshyperlink[\ge]{ple_notation}}
\newcommand\pgt{\glshyperlink[>]{ple_notation}}

\newcommand\posup{\glshyperlink[\sup]{posup_notation}}
\newcommand\hartgamma{\glshyperlink[\gamma]{hartgamma_notation}}

\newcommand\pOmega{\glshyperlink[\Omega]{pOmega_notation}}
\newcommand\pPi{\glshyperlink[\Pi]{pPi_notation}}
\newcommand\arity{\glshyperlink[\alpha]{arity_notation}}
\newcommand\pperp{\glshyperlink[\perp]{pperp_notation}}
\newcommand\pforall{\glshyperlink[\forall]{pforall_notation}}
\newcommand\pimpl{\glshyperlink[\Rightarrow]{pimpl_notation}}

\newcommand\pexists{\glshyperlink[\exists]{pexists_notation}}
\DeclareMathOperator{\FVinternal}{FV}
\newcommand\FV{\glshyperlink[\FVinternal]{FV_notation}}

\newcommand\ssementails{\glshyperlink[\models]{ssementails_notation}}
\newcommand\fsementails{\glshyperlink[\models]{fsementails_notation}}
\def\subst#1[#2/#3]{\glshyperlink[{#1[#2 / #3]}]{subst_notation}}

\newcommand\ssynentails{\glshyperlink[\vdash]{ssynentails_notation}}

\newcommand\pas{\glshyperlink[s]{pas_notation}}
\newcommand\zin{\glshyperlink[\in]{zin_notation}}

\DeclareMathOperator{\TCinternal}{TC}
\newcommand\TC{\glshyperlink[\TCinternal]{TC_notation}}

\DeclareMathOperator{\ONinternal}{ON}
\newcommand\ON{\glshyperlink[\ONinternal]{ON_notation}}

\newcommand\vnh{\glshyperlink[V]{vnh_notation}}
\DeclareMathOperator{\vnhrankinternal}{rank}
\newcommand\vnhrank{\glshyperlink[\vnhrankinternal]{vnhrank_notation}}
\newcommand\ssize{\glshyperlink[\cong]{ssize_notation}}
\DeclareMathOperator{\cardinternal}{card}
\newcommand\card{\glshyperlink[\cardinternal]{card_notation}}
\newcommand\essrank{\operatorname{ess\,rank}}

\newcommand\equivcard{\equiv}
\newcommand\caleph{\aleph}
\newcommand\cle{\le}
\newcommand\cge{\ge}
\newcommand\clt{<}
\newcommand\cgt{>}

\DeclareMathOperator{\diam}{diam}