proposition: Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'.
proof: Proof. intros. generalize (find_1 H) (find_1 H0); clear H H0. intros; rewrite H in H0; injection H0; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface