we also need to go below mkSet for \notin

0b7821f1 · Ralf Jung · 39654079 · 0b7821f1
Commit 0b7821f1 authored Feb 16, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

theories/sets.v theories/sets.v +2 -0

No files found.
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -20,6 +20,8 @@ Proof. by split; [split | |]; repeat intro. Qed.

 Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f.
 Proof. done. Qed.
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ~f x → x ∉ mkSet f.
+Proof. done. Qed.

 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
 Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),