Make initial formation sequences for PL lemma an exercise like it is …

…for FOL.
OpenLogicProject · Dec 15, 2023 · 9d2dbb4 · 9d2dbb4
1 parent 7a56899
commit 9d2dbb4
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/content/propositional-logic/syntax-and-semantics/formation-sequences.tex b/content/propositional-logic/syntax-and-semantics/formation-sequences.tex
@@ -107,6 +107,10 @@
 is a formation sequence for~$!A_k$.
 \end{lem}
 
+\begin{proof}
+Exercise.
+\end{proof}
+
 \begin{thm}
 \ollabel{thm:fseq-frm-equiv}
 $\Frm[L_0]$ is the set of all expressions (strings of symbols)