Enable checking a set of invariants and see which ones broke

[bugarela]

Recently, I came up with this workaround for this problem:

https://github.com/left-curve/left-curve/blob/e0609fbadc7040effd44095926899a2a52a014da/grug/jellyfish-merkle/spec/quint/apply_state_machine.qnt#L370-L391

We should make this built-in into Quint. Users should be able to provide a set (yargs array) of invariants to --invariants and we Quint should print which ones were violated.

Not sure how to do that for Apalache (verify/compile), but even if that's not possible, we should still do it for the simulator (and combine all of them into a conjunction for Apalache).