[ rmk ] One can (re)derive the BagEq solver from the AbMon one

Consider that a list of constants is the join of a list of singletons.
Name these singletons as if they were variables (making sure that equal
values are given the same name) and then run the AbMon solver on them.
Because Lists with BagEq as the underlying equivalence relation define
a commutative monoid, everything is fine. With this method, we gain
handling of list variables for free.

The unelegant thing is that we are not using the Commutative Monoid at
all given that everything is considered a variable. However this gives
us the opportunity to gloat and call this technique a generalization of
the previous one.

The only caveat is that the arguments to the tactics cannot be inferred
by Agda anymore. A bit of quoting machinery could be called for help.