diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 2a45cae7cbd88a1fc94619caf86a6a06aadb95df..5907de36b49d31e65dfd38b5599f27a0b0fc4978 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -212,7 +212,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $ } \end{mathparpagebreakable} -\subsection{Proof rules} +\subsection{Proof Rules} \label{sec:proof-rules} The judgment $\vctx \mid \prop \proves \propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds.