From 183765dd2e1ac36a155305f18fa202d9b5c20650 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sun, 9 Apr 2023 12:08:30 -0600
Subject: [PATCH] Add LaTeX description of lemma 0a.

---
 .../Enderton/Chapter0.tex                     | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 mathematical-introduction-logic/Enderton/Chapter0.tex

diff --git a/mathematical-introduction-logic/Enderton/Chapter0.tex b/mathematical-introduction-logic/Enderton/Chapter0.tex
new file mode 100644
index 0000000..c69f9af
--- /dev/null
+++ b/mathematical-introduction-logic/Enderton/Chapter0.tex
@@ -0,0 +1,22 @@
+\documentclass{article}
+\usepackage{amsfonts, amsthm}
+\usepackage{hyperref}
+
+\newtheorem{theorem}{Theorem}
+
+\begin{document}
+
+\begin{theorem}[Lemma 0A]
+
+Assume that $\langle x_1, \ldots, x_m \rangle = \langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$.
+Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
+
+\end{theorem}
+
+\begin{proof}
+
+\href{Chapter0.lean}{Enderton.Chapter0.lemma\_0a}
+
+\end{proof}
+
+\end{document}