Linting and optimization

2 files changed, 6 insertions, 5 deletions

diff --git a/library/set/regularity.tex b/library/set/regularity.tex
index 794d34f..068d6a8 100644
--- a/library/set/regularity.tex
+++ b/library/set/regularity.tex
@@ -31,7 +31,7 @@
     Then there exists a \in-minimal element of $A$.
 \end{proposition}
 \begin{proof}
-    Follows by \cref{regularity_aux,inhabited}.
+    Follows by \cref{regularity_aux}.
 \end{proof}
 
 
@@ -44,10 +44,11 @@
 \begin{proof}
     \begin{byCase}
         \caseOf{$A = \emptyset$.}
-            Straightforward.
-        \caseOf{$A$ is inhabited.}
-            Take $a$ such that $a$ is a \in-minimal element of $A$.
+            Follows by assumption.
+        \caseOf{$A \neq\emptyset$.}
+            Take $a$ such that $a$ is a \in-minimal element of $A$ by \cref{nonempty_inhabited,regularity}.
             Then for all $x\in a$ we have $x\notin A$.
+            Follows by assumption.
     \end{byCase}
 \end{proof}.
 
diff --git a/library/set/suc.tex b/library/set/suc.tex
index 3776045..ecfa701 100644
--- a/library/set/suc.tex
+++ b/library/set/suc.tex
@@ -1,7 +1,7 @@
 \import{set/cons.tex}
 \import{set/regularity.tex}
 
-\subsection{Successor}
+\subsection{Ordinal successor}
 
 \begin{definition}\label{suc}
     $\suc{x} = \cons{x}{x}$.