proposition: Lemma elements_2 : InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
proof: Proof. unfold MapsTo. rewrite InA_alt. intros ((e0,a),(H,H0)). red in H; simpl in H; unfold E.eq in H; destruct H; subst. apply elements_complete; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface