set_solver does not unfold set_Exist and set_Forall
Lemma foo : set_Exists (.= 10) ({[ 10 ]} : gset nat).
Proof.
Fail set_solver. (* does not work *)
unfold set_Exists. set_solver. (* works *)
Qed.
Lemma foo : set_Exists (.= 10) ({[ 10 ]} : gset nat).
Proof.
Fail set_solver. (* does not work *)
unfold set_Exists. set_solver. (* works *)
Qed.