diff options
Diffstat (limited to 'theories/FSets/FSetProperties.v')
-rw-r--r-- | theories/FSets/FSetProperties.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 2315dc532..f6eebdc17 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -546,7 +546,7 @@ Module Properties (M: S). rewrite leb_1 in H2. rewrite <- elements_iff in H1. assert (~E.eq x y). - swap H; rewrite H3; auto. + contradict H; rewrite H; auto. ME.order. intros. rewrite filter_InA in H1; auto; destruct H1. |