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.

Completed the relevant proofs from Benjamin Pierce's book. The last
big one in full_subtypingScript.sml is quite a complicated beast, with
three inductions.

Split subtypes script up into three parts. One for basic types, and then
one for each of the subtyping relations.

Completed the proof that the algorithmic and original subtyping
relations for kernel Fsub coincide.

Files making up the "fsub" example. It doesn't build yet.