Terms and labelled terms now derived from generic terms.

This is a big change that points to the implementation of a complete
nominal datatype package. The use of generic terms means that we only
need to do one hairy quotient, and one hairy derivation of a recursion
principle.

The recursion principle in question features a new "FCB" (one of the
side-conditions that need to be proved in order to get a recursive
function admitted). Though I think it's better, it can be a little
fiddlier to prove. It's also stronger, so in theory, there may be
reasonable functions that the new FCB rejects. It should certainly be
possible to automate the bulk of the new fiddly proofs.

Changes in computability/lambda caused by name-changes in chapter 2 theory.

Export bstore_thm from reductionEval, and use it in a few more places.

(This is the function that stores a theorem, and adds it to the stateful
lambda-calculus rewriter.)

Simplify proofs through automatic beta-reduction rewrites.

Prove a s-m-n theorem for case m = 1, n = 1 and what Wikipedia refers
to as Kleene's 2nd recursion theorem.

Recast the findleast combinator to take a continuation parameter.
This gives me a way of making things I might want to apply to the rest
of findleast strict (i.e., the non-termination of findleast can't be
masked).

Move some theorems around; mainly to put cfindleast into churchnumTheory.

Add the start of a theory of computable lists, with functions cons,
hd, nil, append and el (nth).

Computable versions of functions detect if an "encoded" term is a
church numeral.

Prove that "Nipkow substitution" (actually used by Shankar, and
probably due to de Bruijn) is computable, and that so too is the
computation a normal order reduct. My universal machine will be
something like "while (not o bnf) noreduct".

Move the computability stuff based on the lambda-calculus into a
separate computability directory, where the lambda-calculus approach
can be a separate sub-directory. This makes room for having other
models (register machines, recursive functions, etc) as sister
sub-directories.