Skip to content

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.