Add theorem's definition to have more context

docs/TS (eager).tex

@@ -6,17 +6,22 @@
 
 \renewcommand{\familydefault}{\sfdefault}
 
+\pagestyle{empty}
+
 \begin{document}
-\[
-e = \lambda v.e_0
-\]
+\paragraph{Teo Sustitución (cálculo-\(\lambda\) eager):} Si \(\llbracket\delta
+w\rrbracket\eta = \eta'w\) para todo \(w \in \textit{FV}(e)\), entonces
+\(\llbracket e/_\delta\rrbracket\eta = \llbracket e\rrbracket \eta'\)
+
+\underline{Caso \(e = \lambda v.\, e_0\)}:
+
 \begin{align*}
   \llbracket(\lambda v.e_0)_{/\delta}\rrbracket\eta &= \llbracket\lambda v_{new} {e_0}_{/[\delta | v:v_{new}]}\rrbracket\eta \label{eq:1}\tag{1}\\
   &= (\iota_\bot \circ \Psi)(\lambda d. \llbracket{e_0}_{/[\delta | v: v_{new}]}\rrbracket [\eta | v_{new}: d])
 \end{align*}
 \eqref{eq:1} donde \(v_{new} \notin \bigcup_{w\in FV(e_0)-\{v\}}FV(\delta w)\)
 
-\noindent\rule{2cm}{0.4pt}
+\rule{2cm}{0.4pt}
 
 \[\llbracket\lambda v. e_0\rrbracket\eta' = (\iota_\bot \circ \Psi)(\lambda d. \llbracket e_0\rrbracket[\eta' | v: d])\]
 debemos ver que:
@@ -30,7 +35,7 @@ p/usar \(H.I.\)
   &= \iota_\bot d
 \end{align*}
 
-\noindent\rule{2cm}{0.4pt}
+\rule{2cm}{0.4pt}
 
 \[\iota_\bot \eta'_0 w = \iota_\bot[\eta' | v: d]w \underset{\mathclap{\overbrace{\text{si}\, v=w}{}}}{=} \iota_\bot d\]
 
@@ -39,4 +44,4 @@ p/usar \(H.I.\)
 
 \[\iota_\bot[\eta'| v: d]w \underset{\mathclap{\overbrace{v\neq w}{}}}{=} \boxed{\iota_\bot\eta'w}\]
 
-\end{document}
+\end{document}