Make renaming not generate as many new scopetags #148
Description
There are new features for renaming in the pipeline (#147 and #146) which suffer from a common problem of generating completely fresh ScopeTags for the renamed theory. Consider the following scenario:
We rename * to + in both ThGrp and ThAbGrp (which extends ThGrp with a commutativity axiom). With the present setup, it will not be the case that ThAddGrp will be a proper inclusion of ThAddAbGrp.
One way to address this is to make the data to rename ThGrp (resp. ThAbGrp) be the renaming morphism (as generated by the existing tooling) from ThMon to ThAddMon as well as an inclusion from ThMon into ThGrp (resp ThAbGrp). This fancier renaming function will make sure to use the fresh scopetags from ThAddMon in both ThAddGrp and ThAddAbGrp.
