This way, type class search will fail immediately on first type
class constraint of any of the `fin_map_dom` lemmas if no `Dom`
can be found.