diff options
Diffstat (limited to 'theories/FSets/FMapIntMap.v')
| -rw-r--r-- | theories/FSets/FMapIntMap.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v index 6ad24f1cc..b5fe6722b 100644 --- a/theories/FSets/FMapIntMap.v +++ b/theories/FSets/FMapIntMap.v @@ -258,7 +258,13 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. apply alist_sorted_sort. apply alist_of_Map_sorts. Qed. - + + Lemma elements_3w : NoDupA eq_key (elements m). + Proof. + change eq_key with (@PE.eqk A). + apply PE.Sort_NoDupA; apply elements_3; auto. + Qed. + Lemma elements_1 : MapsTo x e m -> InA eq_key_elt (x,e) (elements m). Proof. |