diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index 912efc8..cd36fcc 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -1114,7 +1114,7 @@ List all the members of $V_4$.
 \section{Algebra of Sets}%
 \hyperlabel{sec:algebra-sets}
 
-\subsection{\verified{Commutative Laws}}%
+\subsection{\pending{Commutative Laws}}%
 \hyperlabel{sub:commutative-laws}
 
 For any sets $A$ and $B$,
@@ -1160,7 +1160,7 @@ For any sets $A$ and $B$,
 
 \end{proof}
 
-\subsection{\verified{Associative Laws}}%
+\subsection{\pending{Associative Laws}}%
 \hyperlabel{sub:associative-laws}
 
 For any sets $A$, $B$ and $C$,
@@ -1217,7 +1217,7 @@ For any sets $A$, $B$ and $C$,
 
 \end{proof}
 
-\subsection{\verified{Distributive Laws}}%
+\subsection{\pending{Distributive Laws}}%
 \hyperlabel{sub:distributive-laws}
 
 For any sets $A$, $B$, and $C$,
@@ -1273,7 +1273,7 @@ For any sets $A$, $B$, and $C$,
 
 \end{proof}
 
-\subsection{\verified{De Morgan's Laws}}%
+\subsection{\pending{De Morgan's Laws}}%
 \hyperlabel{sub:de-morgans-laws}
 
 For any sets $A$, $B$, and $C$,
@@ -1331,7 +1331,7 @@ For any sets $A$, $B$, and $C$,
 
 \end{proof}
 
-\subsection{\verified{%
+\subsection{\pending{%
   Identities Involving \texorpdfstring{$\emptyset$}{the Empty Set}}}%
 \hyperlabel{sub:identitives-involving-empty-set}
 
@@ -1401,7 +1401,7 @@ For any set $A$,
 
 \end{proof}
 
-\subsection{\verified{Monotonicity}}%
+\subsection{\pending{Monotonicity}}%
 \hyperlabel{sub:monotonicity}
 
 For any sets $A$, $B$, and $C$,
@@ -1474,7 +1474,7 @@ For any sets $A$, $B$, and $C$,
 
 \end{proof}
 
-\subsection{\verified{Anti-monotonicity}}%
+\subsection{\pending{Anti-monotonicity}}%
 \hyperlabel{sub:anti-monotonicity}
 
 For any sets $A$, $B$, and $C$,
@@ -1644,7 +1644,7 @@ For any set $C$ and $\mathscr{A} \neq \emptyset$,
 
 \end{proof}
 
-\subsection{\verified{%
+\subsection{\pending{%
   \texorpdfstring{$\cap$/$-$}{Intersection/Difference} Associativity}}%
 \hyperlabel{sub:intersection-difference-associativity}
 
@@ -2187,7 +2187,7 @@ Show by example that for some sets $A$, $B$, and $C$, the set $A - (B - C)$ is
 
 \end{proof}
 
-\subsection{\verified{Exercise 2.15a}}%
+\subsection{\pending{Exercise 2.15a}}%
 \hyperlabel{sub:exercise-2.15a}
 
 Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$.
@@ -2224,7 +2224,7 @@ Show that $A \cap (B + C) = (A \cap B) + (A \cap C)$.
 
 \end{proof}
 
-\subsection{\verified{Exercise 2.15b}}%
+\subsection{\pending{Exercise 2.15b}}%
 \hyperlabel{sub:exercise-2.15b}
 
 Show that $A + (B + C) = (A + B) + C$.
@@ -2914,7 +2914,7 @@ If not, then under what conditions does equality hold?
 
 \end{proof}
 
-\subsection{\verified{Corollary 3C}}%
+\subsection{\pending{Corollary 3C}}%
 \hyperlabel{sub:corollary-3c}
 
 \begin{theorem}[3C]
@@ -3730,7 +3730,8 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Bookshelf/Enderton/Set/Relation}{Set.Relation.modEquiv\_partition}
+  \lean{Bookshelf/Enderton/Set/Relation}
+    {Set.Relation.modEquiv\_partition}
 
   Let $\Pi = \{[x]_R \mid x \in A\}$.
   We show that (i) there are no empty sets in $\Pi$, (ii) no two different sets
@@ -4345,7 +4346,7 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
 
 \end{answer}
 
-\subsection{\verified{Exercise 3.11}}%
+\subsection{\pending{Exercise 3.11}}%
 \hyperlabel{sub:exercise-3.11}
 
 Prove the following version (for functions) of the extensionality principle:
@@ -6527,7 +6528,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 \section{Arithmetic}%
 \hyperlabel{sec:arithmetic}
 
-\subsection{\verified{Theorem 4I}}
+\subsection{\pending{Theorem 4I}}
 \hyperlabel{sub:theorem-4i}
 
 \begin{theorem}[4I]
@@ -6563,7 +6564,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4J}}
+\subsection{\pending{Theorem 4J}}
 \hyperlabel{sub:theorem-4j}
 
 \begin{theorem}[4J]
@@ -6597,7 +6598,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Left Additive Identity}}%
+\subsection{\pending{Left Additive Identity}}%
 \hyperlabel{sub:left-additive-identity}
 
 \begin{lemma}
@@ -6639,7 +6640,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Lemma 3}}%
+\subsection{\pending{Lemma 3}}%
 \hyperlabel{sub:lemma-3}
 \hyperlabel{sub:succ-add-eq-add-succ}
 
@@ -6683,7 +6684,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4K-1}}%
+\subsection{\pending{Theorem 4K-1}}%
 \label{sub:theorem-4k-1}
 
 \begin{theorem}[4K-1]
@@ -6739,7 +6740,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4K-2}}%
+\subsection{\pending{Theorem 4K-2}}%
 \label{sub:theorem-4k-2}
 
 \begin{theorem}[4K-2]
@@ -6791,7 +6792,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Zero Multiplicand}}%
+\subsection{\pending{Zero Multiplicand}}%
 \hyperlabel{sub:zero-multiplicand}
 
 \begin{lemma}
@@ -6841,7 +6842,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Successor Distribution}}%
+\subsection{\pending{Successor Distribution}}%
 \hyperlabel{sub:successor-distribution}
 
 \begin{lemma}
@@ -6897,7 +6898,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4K-3}}
+\subsection{\pending{Theorem 4K-3}}
 \hyperlabel{sub:theorem-4k-3}
 
 \begin{theorem}[4K-3]
@@ -6958,7 +6959,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Successor Identity}}%
+\subsection{\pending{Successor Identity}}%
 \hyperlabel{sub:successor-identity}
 
 \begin{lemma}
@@ -7011,7 +7012,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Right Multiplicative Identity}}%
+\subsection{\pending{Right Multiplicative Identity}}%
 \hyperlabel{sub:right-multiplicative-identity}
 
 \begin{lemma}
@@ -7062,7 +7063,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4K-5}}
+\subsection{\pending{Theorem 4K-5}}
 \hyperlabel{sub:theorem-4k-5}
 
 \begin{theorem}[4K-5]
@@ -7122,7 +7123,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4K-4}}%
+\subsection{\pending{Theorem 4K-4}}%
 \hyperlabel{sub:theorem-4k-4}
 
 \begin{theorem}[4K-4]
@@ -7180,7 +7181,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 \section{Ordering on \texorpdfstring{$\omega$}{Natural Numbers}}%
 \hyperlabel{sec:ordering-natural-numbers}
 
-\subsection{\verified{Ordering on Successor}}%
+\subsection{\pending{Ordering on Successor}}%
 \hyperlabel{sub:ordering-successor}
 
 \begin{lemma}
@@ -7226,7 +7227,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Lemma 4L(a)}}%
+\subsection{\pending{Lemma 4L(a)}}%
 \hyperlabel{sub:lemma-4l-a}
 
 \begin{lemma}[4L(a)]
@@ -7294,7 +7295,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Lemma 4L(b)}}%
+\subsection{\pending{Lemma 4L(b)}}%
 \hyperlabel{sub:lemma-4l-b}
 
 \begin{lemma}[4L(b)]
@@ -7577,7 +7578,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Theorem 4N}}%
+\subsection{\pending{Theorem 4N}}%
 \hyperlabel{sub:theorem-4n}
 
 \begin{theorem}[4N]
@@ -7695,7 +7696,7 @@ Show that $<_L$ is a linear ordering on $A \times B$.
 
 \end{proof}
 
-\subsection{\verified{Corollary 4P}}%
+\subsection{\pending{Corollary 4P}}%
 \hyperlabel{sub:corollary-4p}
 
 \begin{corollary}[4P]
@@ -8320,7 +8321,7 @@ Complete the proof of \nameref{sub:theorem-4k-5}.
 
 \end{proof}
 
-\subsection{\verified{Exercise 4.17}}%
+\subsection{\pending{Exercise 4.17}}%
 \hyperlabel{sub:exercise-4.17}
 
 Prove that $m^{n+p} = m^n \cdot m^p$.