Improve notation of HOL schemas

Author: v--

text/dependent_types.tex

@@ -423,9 +423,9 @@ \section{Dependent types}\label{sec:dependent_types}
     Streicher proves that the reflection rule is incompatible with \fullref{thm:church_rosser_theorem}.
 
     \thmitem{def:identity_type/j}\mcite[50]{UnivalentFoundationsProgram2013HoTT} The following \hyperref[rem:type_theory_rule_classification/elim]{elimination rule}, based on the constant \( \synJ \), is much more complicated:
-    \small
+    \footnotesize
     \begin{equation*}\taglabel[\ensuremath{ =_-^J }]{inf:def:identity_type/j/elim}
-      \begin{prooftree}[separation=1em]
+      \begin{prooftree}[separation=1.5em]
         \hypo{ x: \tau }
         \hypo{ y: \tau }
         \hypo{ p: x \syneq_{\tau} y }
@@ -450,7 +450,7 @@ \section{Dependent types}\label{sec:dependent_types}
     We also have the following \hyperref[rem:type_theory_rule_classification/equality/comp]{computation rule} based on \cite[\S A.2.10]{UnivalentFoundationsProgram2013HoTT}:
     \small
     \begin{equation*}\taglabel[\ensuremath{ =_\beta^J }]{inf:def:identity_type/j/comp}
-      \begin{prooftree}
+      \begin{prooftree}[separation=1.2em]
         \hypo{ x: \tau }
         \hypo{ y: \tau }
         \hypo{ p: x \syneq_{\tau} y }
@@ -469,8 +469,9 @@ \section{Dependent types}\label{sec:dependent_types}
     \incite*[\S 9.1.3]{Mimram2020ProgramEqualsProof} additionally provides a straightforward uniqueness rule, however he claims it is \enquote{debatable} because, as shown in \cite[thm. 1]{Streicher1993IntensionalTypeTheory}, uniqueness entails the reflection rule. In particular, the uniqueness rule is not present in \cite[\S A.2.10]{UnivalentFoundationsProgram2013HoTT}.
 
     \thmitem{def:identity_type/k}\mcite[13]{Streicher1993IntensionalTypeTheory} Streicher suggests the following alternative to \ref{inf:def:identity_type/j/elim}:
+    \small
     \begin{equation*}\taglabel[\ensuremath{ =_-^K }]{inf:def:identity_type/k/elim}
-      \begin{prooftree}[separation=1.3em]
+      \begin{prooftree}
         \hypo{ x: \tau }
         \hypo{ p: x \syneq_{\tau} x }
         \infer[dashed]2{ \sigma: \BbbT }
@@ -484,6 +485,7 @@ \section{Dependent types}\label{sec:dependent_types}
         \infer4[\ref{inf:def:identity_type/k/elim}]{ \syn\Kappa (\qabs {x^{\tau}} \qabs {p^{x \syneq_{\tau} x}} \sigma) (\qabs {z^{\tau}} M) A E: \sigma[x \mapsto A, p \mapsto E] }
       \end{prooftree}
     \end{equation*}
+    \normalsize
 
     Correspondingly, we have the following computation rule:
     \begin{equation*}\taglabel[\ensuremath{ =_\beta^K }]{inf:def:identity_type/k/comp}
@@ -1178,9 +1180,9 @@ \section{Dependent types}\label{sec:dependent_types}
   \Cref{thm:unit_type_term_uniqueness} shows how to derive a term of type \( \synx \syneq_{\syn\Bbbone} \synU_+ \). We will find it more convenient to swap the two sides (which is justified by \cref{thm:propositional_equality_equivalence_relation/symmetry}).
 
   Let \( M: \synU_+ \syneq_{\syn\Bbbone} \synx \). We can then construct the following derivation:
-  \small
+  \footnotesize
   \begin{equation*}
-    \begin{prooftree}[separation=1em]
+    \begin{prooftree}
       \infer0[\ref{inf:def:dependent_unit_type/form}]{ \syn\Bbbone: \syn\BbbT }
 
       \infer0[\ref{inf:def:dependent_unit_type/form}]{ \syn\Bbbone: \syn\BbbT }