proposition: Lemma mapsto_fun {elt} m x (e e':elt) : MapsTo x e m -> MapsTo x e' m -> e=e'.
proof: Proof. rewrite <- !find_spec. congruence. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)