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/FMapWeakFacts.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

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

diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index f53e1d2b5c..af8dccf536 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -326,6 +326,22 @@ rewrite <- H0; rewrite H2; rewrite H1; auto.
 auto.
 Qed.
 
+Lemma empty_o : forall x, find x (empty elt) = None.
+Proof.
+intros.
+case_eq (find x (empty elt)); intros; auto.
+generalize (find_2 H).
+rewrite empty_mapsto_iff; intuition.
+Qed.
+
+Lemma empty_a : forall x, mem x (empty elt) = false.
+Proof.
+intros.
+case_eq (mem x (empty elt)); intros; auto.
+generalize (mem_2 H).
+rewrite empty_in_iff; intuition.
+Qed.
+
 Lemma add_eq_o : forall m x y e, 
  E.eq x y -> find y (add x e m) = Some e.
 Proof.
-- 
cgit v1.2.3