rename should only affect variables

[mn200]

Currently rename will abbreviate in lossy fashion such that

rename [‘SUC n’]

when applied to a goal with conclusion

SUC (2 + x * y + z) < 101

will turn this into

SUC n < 101

rather than failing (or finding a SUC var instance in the assumptions). Nor will this introduce an abbreviation assumption telling you what n used to be.

We should provide a new entry-point for the old behaviour.