From ae1dd86c271eea87d8a56919ad531ef38cf6e0fe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Feb 2019 19:20:02 +0100
Subject: [PATCH] Support `elements` in `set_solver`.

---
 theories/fin_sets.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 11789c4a..932ff62f 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -35,6 +35,10 @@ Proof.
 Defined.
 
 (** * The [elements] operation *)
+Global Instance set_unfold_elements X x P :
+  SetUnfold (x ∈ X) P → SetUnfold (x ∈ elements X) P.
+Proof. constructor. by rewrite elem_of_elements, (set_unfold (x ∈ X) P). Qed.
+
 Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
 Proof.
   intros ?? E. apply NoDup_Permutation.
-- 
GitLab