Simplification and improvement of "subst x" in such a way that it
works in the presence of local definitions referring to x and
dependent in other hyps or concl.

Fixes bug #3297.