From cc4ff17643ac0bb7f099566b813df671c3c751f8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Apr 2015 21:22:35 +0200
Subject: [PATCH] Add switch (including unstructured variants such as Duff's
 device).

---
 theories/collections.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index c7b1e426..41e7ec53 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -113,6 +113,9 @@ Section collection_monad_base.
     unfold mguard, collection_guard; simpl; case_match;
       rewrite ?elem_of_empty; naive_solver.
   Qed.
+  Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
+    P → x ∈ X → x ∈ guard P; X.
+  Proof. by rewrite elem_of_guard. Qed.
   Lemma guard_empty `{Decision P} {A} (X : M A) : guard P; X ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
   Proof.
     rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
-- 
GitLab