From 6ca6bef6e701703ce38b89b81c89a61b2db3cb47 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 31 May 2006 21:55:30 +0000
Subject: petits ajouts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FSetWeakFacts.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'theories/FSets/FSetWeakFacts.v')

diff --git a/theories/FSets/FSetWeakFacts.v b/theories/FSets/FSetWeakFacts.v
index c5e82e09c8..798a3f8559 100644
--- a/theories/FSets/FSetWeakFacts.v
+++ b/theories/FSets/FSetWeakFacts.v
@@ -159,6 +159,12 @@ generalize (mem_iff s x) (mem_iff s y)(In_eq_iff s H).
 destruct (mem x s); destruct (mem y s); intuition.
 Qed.
 
+Lemma empty_b : mem y empty = false.
+Proof.
+generalize (empty_iff y)(mem_iff empty y).
+destruct (mem y empty); intuition.
+Qed.
+
 Lemma add_b : mem y (add x s) = eqb x y || mem y s.
 Proof.
 generalize (mem_iff (add x s) y)(mem_iff s y)(add_iff s x y); unfold eqb.
-- 
cgit v1.2.3