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. rewrite mem_1 in *; auto; discriminate. - intros ? ? Hk _ _ _; rewrite Hk; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface