Simplify `dom` even further.
Passed
Robbert Krebbers
created pipeline for commit
85d5c299
, finished
Related merge request !476 to merge robbert/mapset_dom_with
5 minutes 0 seconds, queued for 1 seconds