diff options
Diffstat (limited to 'theories/FSets/FSetToFiniteSet.v')
| -rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 747fd3796..de483f158 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -107,8 +107,8 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; unfold E.eq in *; auto with sets. split; auto. - swap H1. - inversion H2; auto. + contradict H1. + inversion H1; auto. Qed. Lemma mkEns_Finite : forall s, Finite _ (!!s). |