FSets: integration of suggestions by P. Casteran and S. Lescuyer

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11698 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 8c692bd07..dac78c596 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -476,6 +476,14 @@ Proof.
 unfold Equal; intros; repeat rewrite filter_iff; auto; rewrite H0; tauto.
 Qed.
 
+Lemma filter_ext : forall f f', compat_bool E.eq f -> (forall x, f x = f' x) ->
+ forall s s', s[=]s' -> filter f s [=] filter f' s'.
+Proof.
+intros f f' Hf Hff' s s' Hss' x. do 2 (rewrite filter_iff; auto).
+rewrite Hff', Hss'; intuition.
+red; intros; rewrite <- 2 Hff'; auto.
+Qed.
+
 Lemma filter_subset : forall f, compat_bool E.eq f -> 
   forall s s', s[<=]s' -> filter f s [<=] filter f s'.
 Proof.