1343 overlap obligation

fixes #1342 by renaming variables if a clash is possible.

@mcodescu please review (this patch will clash with #1337)
Checking for type preserving substitutions is not necessary. (I tested this in a separate branch.)
Variables are unique by name within a given scope. Inner variables shadow outer variables with the same name without regarding their sorts.