proposition: Lemma elements_1 : MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
proof: Proof. unfold MapsTo. rewrite InA_alt. intro H. exists (x,e). split. - red; simpl; unfold E.eq; auto. - apply elements_correct; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface