doc-src/TutorialI/Rules/rules.tex

 \index{substitution|)}
 
 
 \section{Quantifiers}
 
-\index{quantifiers|(}\index{quantifiers!universal|(}%
+\index{quantifiers!universal|(}%
 Quantifiers require formalizing syntactic substitution and the notion of 
 arbitrary value.  Consider the universal quantifier.  In a logic
 book, its introduction  rule looks like this: 
 \[ \infer{\forall x.\,P}{P} \]
 Typically, a proviso written in English says that $x$ must not

 Prove the lemma
 \[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
 \emph{Hint}: the proof is similar 
 to the one just above for the universal quantifier. 
 \end{exercise}
-\index{quantifiers|)}\index{quantifiers!existential|)}
+\index{quantifiers!existential|)}
 
 
 \subsection{Renaming an Assumption: {\tt\slshape rename_tac}}
 
 \index{assumptions!renaming|(}\index{*rename_tac (method)|(}%