diff -r e3752aac8ec2 -r dd9dde2d902b ChengsongTanPhdThesis/Chapters/Finite.tex
--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Sat Dec 24 11:55:04 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Fri Dec 30 01:52:32 2022 +0000
@@ -2075,8 +2075,10 @@
 \begin{proof}
 	By induction on $a$. $rs$ is set to take arbitrary values.
 \end{proof}
-It is also not surprising that $\textit{rsimp}$ will cover
-the effect of $\hflataux{\_}$:
+It is also not surprising that 
+two regular expressions differing only in terms
+of the
+nesting of parentheses are equivalent w.r.t. $\textit{rsimp}$:
 \begin{lemma}\label{cbsHfauRsimpeq1}
 	$\rsimp{(r_1 + r_2)} = \rsimp{(\RALTS{\hflataux{r_1} @ \hflataux{r_2}})}$
 \end{lemma}