Improved performance of type-class resolution.

Modified the treatment of substitution over a meta-var. There is still an issue to be fixed: substitutions need to be inverted only when they come from the open operation of a term with a binder.

Now type-class instances can appear in the local context as well as the global context.