@@ -360,14 +360,14 @@ They are declared as follows (again, in the prelude):
360\begin{SaveVerbatim}{findecl}
360\begin{SaveVerbatim}{findecl}
362data Fin : Nat -> Type where
362data Fin : Nat -> Type where
363− fO : Fin (S k)
363+ fZ : Fin (S k)
364 fS : Fin k -> Fin (S k)
364 fS : Fin k -> Fin (S k)
366\end{SaveVerbatim}
366\end{SaveVerbatim}
367\useverb{findecl}
367\useverb{findecl}
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;
371\texttt{fS n} is the
371\texttt{fS n} is the
372\texttt{n+1}th element of a finite set with \texttt{S k} elements.
372\texttt{n+1}th element of a finite set with \texttt{S k} elements.
373\tTC{Fin} is indexed by a \tTC{Nat}, which
373\tTC{Fin} is indexed by a \tTC{Nat}, which