From ff0750f533d09fc753d97e4cee18486b21cd5c3b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Jun 2019 23:40:46 +0200
Subject: [PATCH] Prove `set_Forall_list_to_set`.

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

diff --git a/theories/sets.v b/theories/sets.v
index ff784222..b2ef0b20 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -885,6 +885,8 @@ Section quantifiers.
   Proof. unfold set_Forall. set_solver. Qed.
   Lemma set_Forall_union_inv_2 X Y : set_Forall P (X ∪ Y) → set_Forall P Y.
   Proof. unfold set_Forall. set_solver. Qed.
+  Lemma set_Forall_list_to_set l : set_Forall P (list_to_set (C:=C) l) ↔ Forall P l.
+  Proof. rewrite Forall_forall. unfold set_Forall. set_solver. Qed.
 
   Lemma set_Exists_empty : ¬set_Exists P (∅ : C).
   Proof. unfold set_Exists. set_solver. Qed.
@@ -897,6 +899,8 @@ Section quantifiers.
   Lemma set_Exists_union_inv X Y :
     set_Exists P (X ∪ Y) → set_Exists P X ∨ set_Exists P Y.
   Proof. unfold set_Exists. set_solver. Qed.
+  Lemma set_Exists_list_to_set l : set_Exists P (list_to_set (C:=C) l) ↔ Exists P l.
+  Proof. rewrite Exists_exists. unfold set_Exists. set_solver. Qed.
 End quantifiers.
 
 Section more_quantifiers.
-- 
GitLab