Bags standard module overridden by TLAPS, exports extra bag unrelated declarations

There appears to be some "weirdness", for lack of a better term, going on with the Bags module when using TLAPS.

\* What happened ***

Extending "Bags" in an own module resulted in a duplication error with a "Reverse" operator that I had defined. This was unexpected, since the Standard Module bags shouldn't define such an operator.

\* The problem with Bags and TLAPS ***

For some reason, TLAPS includes a "Bags" module. This module consists of an exact copy of the standard "Bags" plus some extras, the latter consisting of:
1. extension of modules: TLAPS, FiniteSetTheorems, SequenceTheorems
2. definition of a SeqToBag operator
3. proofs of various properties on Bags

The extended "SequenceTheorems" module in particular, defines "Reverse" as well as various other common operations on Sequences (likewise for FiniteSetTheorems). These definitions are therefore, by extension, in TLAPS' "Bags" module.

The TLA+ library path locations, in the toolbox "preference" settings, appear to take precedence over the Standard Modules toolbox itself provides. Therefore, when the TLAPS library is included, extending "Bags" means extending TLAPS' "Bags", which includes various operations on lists and sets.

\* Other Standard Modules in TLAPS ***

"RealTime" and "FiniteSets" are also provided by TLAPS. However these are exact copies (except for comments).

Note that unlike with "Bags", the theorems and proofs for "FiniteSets" are in the "FiniteSetTheorems" and "FiniteSetTheorems_proofs" modules (which extend FiniteSets).

Note also that no "Sequences" module is provided by TLAPS, yet there is a "SequenceTheorems" module that extends the standard "Sequences" module provided by toolbox.

\* Possible fixes ***

This situation seems easily avoidable:

Firstly, the extra (non-standard) content of TLAPS "Bags" should be moved to a "BagTheorems" module (and possibly "BagTheorems_proof"), matching the approach followed in "FiniteSets" and "RealTime". Secondly, should there be no need for copies of standard modules in TLAPS these should be removed, matching the approach followed in "SequenceTheorems".

Finally, a couple of points regarding toolbox:

It doesn't seem quite right that toolbox would allow for standard modules to be overridden silently. Maybe a warning should be provided? Regarding usability. The error message I got did include a line indicating that "Reverse" was duplicating a declaration in "SequenceTheorems". It would be nice if one could access this source by clicking this line in the error message (instead it takes us to the duplication in one's own file).