proposition: Lemma restrict_mapsto_iff : forall m m' k e, MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'.
proof: Proof. intros m m' k e. unfold restrict. rewrite filter_iff. - intuition. - intros ? ? Hk _ _ _; rewrite Hk; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface