proposition: Lemma diff_mapsto_iff : forall m m' k e, MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'.
proof: Proof. intros m m' k e. unfold diff. rewrite filter_iff. intuition (auto with map bool). rewrite mem_1 in *; auto; discriminate. intros ? ? Hk _ _ _; rewrite Hk; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)