diff --git a/dist/naturaldeduction.html b/dist/naturaldeduction.html
index 21be6d1..6b1df93 100644
--- a/dist/naturaldeduction.html
+++ b/dist/naturaldeduction.html
@@ -207,7 +207,7 @@ <h2>First-order logic</h2>
 
 <h3>Examples of direct applications of rules</h3>
 
-
+<h4>Existential quantifier</h4>
 
   <textarea proofSystem="NaturalDeduction">
   Q(x) |- P(a)  *
@@ -231,6 +231,7 @@ <h3>Examples of direct applications of rules</h3>
   Q(x) |- p
 </textarea>
 
+<h4>Universal quantifier</h4>
 
 If you proved <code>P(x)</code> and the hypothesis do not depend on <code>x</code>, then you deduce <code>forall x P(x)</code>. That rule is called the introduction of <code>forall</code>.
   <textarea proofSystem="NaturalDeduction">