finite types

[DanGrayson]

Rewrite finite types section (\subsection{Finite types}) by putting things into environments.

Maybe refer forward to \section{The type of finite types} and to \label{lem:isset-bool}.

[DanGrayson]

This helps #65 by adding what the student needs to do it.

[DanGrayson]

Also move the argument about succ to a new subsection on paths in inductive types, just after this on, and get that exercise about injectivity of succ moved here.