Support for `dom` on multisets in `multiset_solver`/`set_solver`

I would expect the following goal to be solved automatically by either multiset_solver or set_solver, but neither are able to do this:

Lemma example x (xs : gmultiset nat) : x ∈ dom xs → x ∈ xs.
Proof.
  Fail multiset_solver.
  Fail set_solver.
  apply gmultiset_elem_of_dom.
Qed.

changed title from Support for dom on multisets to multiset_solver/set_solver to Support for dom on multisets in multiset_solver/set_solver

This should be easy to support by adding a missing SetUnfold instance for dom. (Which might not be the most informative name for converting a multiset into a set.)

I agree that dom is confusing. What about just multiset_to_set?

dom already works like that, right? Not sure if it's worth renaming, and it's orthogonal to this issue. Just adding the instance should be enough to solve this issue.

mentioned in merge request !591 (merged)

Fixed by !591 (merged)

closed