Type class inference issue with `dom` and `exist_fresh`
From stdpp Require Import fin_sets gmap.
Lemma foo (m : gmap nat nat) : True.
Proof.
destruct (exist_fresh (dom m)).
(*
Unable to satisfy the following constraints:
In environment:
m : gmap nat nat
?Dom : "Dom (gmap nat nat) (mapset.mapset' (pmap.Pmap ()))"
*)
Edited by Robbert Krebbers