Remove generalisation of nested lets from type system

Commented out, and in proofs marked with COMPLETENESS. Basically, the
type system supported generalisation of nested lets, but the inferencer
does not. To prove completeness of the inferencer, we must therefore
remove the (unused) feature from the type system.