Many improvements to `multiset_solver`

1. Support ∈
2. Support ⊂
3. Support case splitting on multiplicity x {[ y ]}, but only do this when there's no other way.

With the improved multiset_solver I am able to solve pretty much all lemmas in the gmultiset file automatically (apart from those that involve elements, size, and other connectives that are out of scope).

The new version also handles @fpottier's test case x ∈ X → {[x]} ⊆ X from #86 (closed).

In addition, I added a bunch of other test cases.