@@ -360,14 +360,14 @@ They are declared as follows (again, in the prelude):
360360\begin{SaveVerbatim}{findecl}
361361
362362data Fin : Nat -> Type where
363− fO : Fin (S k)
363+ fZ : Fin (S k)
364364 fS : Fin k -> Fin (S k)
365365
366366\end{SaveVerbatim}
367367\useverb{findecl}
368368
369369\noindent
370−\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
370+\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements;
371371\texttt{fS n} is the
372372\texttt{n+1}th element of a finite set with \texttt{S k} elements.
373373\tTC{Fin} is indexed by a \tTC{Nat}, which