From 0274e797162cd62fe9145436a66027a61d727d64 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 25 Apr 2006 22:39:38 +0000
Subject: un lemme de double inclusion

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

diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 4aeda775c7..4d8a78a14b 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -154,6 +154,11 @@ Module Properties (M: S).
   Proof.
   unfold Subset; intuition.
   Qed.
+ 
+  Lemma double_inclusion : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1.
+  Proof.
+  unfold Subset, Equal; split; intros; intuition; generalize (H a); intuition.
+  Qed.
 
   (** properties of [empty] *)
 
-- 
cgit v1.2.3