Skip to content

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.