proposition: Lemma add_mapsto_new m x y e e' : ~In x m -> MapsTo y e' (add x e m) <-> (K.eq x y /\ e=e') \/ MapsTo y e' m.
proof: Proof. intros. rewrite add_mapsto_iff. intuition. right; split; trivial. contradict H. exists e'. now rewrite H. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)