diff options
Diffstat (limited to 'theories/MSets/MSetProperties.v')
| -rw-r--r-- | theories/MSets/MSetProperties.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 0f24d76a..396067b5 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -831,7 +831,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). rewrite (inter_subset_equal H). generalize (@cardinal_inv_1 (diff s' s)). destruct (cardinal (diff s' s)). - intro H2; destruct (H2 (refl_equal _) x). + intro H2; destruct (H2 (eq_refl _) x). set_iff; auto. intros _. change (0 + cardinal s < S n + cardinal s). |