Add basic support for `dom` in `set_solver`

It could be nice to have some support for dom in set_solver. One kind of goal I'd be typically interested in is e.g.:

{[ru; rv]} ⊆ dom (gset RegName) (<[ru := v]> (<[rv := w]> ∅))

(which can currently be proved by rewrite !dom_insert; set_solver+).