minor changes in pdf doc

doc/epsilon0-chapter.tex

@@ -659,7 +659,7 @@ \subsubsection{A first attempt}
  $\alpha=\texttt{cons $\beta\;n\;\gamma$}$, and assume that \(\beta\) and \(\gamma\) are \texttt{LT}-accessible.
 In order to prove the accessibility of $\alpha$, we have to consider
 any well formed term \(\delta\) such that \(\delta<\alpha\). 
-But nothing guarantees that \(\delta\)  is strictly  less than \(\beta\) nor \(\gamma\), and we cannot use the induction hypotheses on   \(\beta\) nor \(\gamma\).
+% But nothing guarantees that \(\delta\)  is strictly  less than \(\beta\) nor \(\gamma\), and we cannot use the induction hypotheses on   \(\beta\) nor \(\gamma\).
 
 \input{movies/snippets/T1/wfLTBada}
 
@@ -713,7 +713,7 @@ \subsubsection{Using a stronger inductive predicate.}
 
 \inputsnippets{T1/betaAcc}
 
-The lemma \texttt{betaAcc} allows us to prove by well-founded induction on $\beta$, 
+The new hypothesis  \texttt{beta\_Acc} allows us to prove by well-founded induction on $\beta$, 
 and natural induction on $n$ that (\texttt{cons $\alpha$ $n$ $\beta$}) is accessible.
 
 \inputsnippets{T1/useBetaAcc}
@@ -730,6 +730,7 @@ \subsubsection{Using a stronger inductive predicate.}
 
 \input{movies/snippets/T1/T1Wf}
 
+\subsection{Transfinite induction}
 \index{maths}{Transfinite induction}