1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
but the case Meta(i) vs (Appl (Meta(j),...)) that reduces to Meta(i) was
not. As a result, a tempeted self assegniment yielded strange errors.
Fixed by more aggressively unwinding the subst during fo_unif.
2) Major re-organization of the code to gain some speed in Oliboni's stuff.
The idea is that of introducing a new internal exception KeepReducing
used to signal that, after a fo_unif, it still makes sense to fall back
to machines. Only if it does not it makes sense to distinguish between
Failures and Uncertain and the latter test can now be implemented more
lazily w.r.t. the old version that used to call metas_of_term on the
unwinded machines (that are potentially HUGE).
With this modification, all Oliboni's tests terminate, even if they are
still very slow compared to the height=0 strategy. Moreover, the tests
show that unification on closed terms can still be 4x slower than conversion,
which is partially unexpected.