Potential performance improvement + better disambiguation error messages:

Potential performance improvement + better disambiguation error messages:
the delift functions used to raise Uncertain every time it failed; now it
raises Failure when the local context contains no Metas (that means that
for every future subst it will not contain new Rels).
Note: if we are working up to conversion (I do not think so), we should check
that the local context is Meta-closed, that is a weaker check.