Redefine capture avoiding substitution recursively

[chrisbanks]

Capture avoiding substitution needs redefining.

Note from Ian:
"The possible questions on the alpha-conversion are to do with you having an implementation working almost entirely at the top level, rather than recursively down the structure of terms. All of the detailed operations are done recursively, of course --- free names, bound names, renaming --- but the strategy for capture avoidance is to call each of those from the top level, rather than, say, define capture-avoiding renaming directly by recursion. I think it's safe, but there are some curiosities. For example, when a name appears in a term both bound and free, in different subterms."