proposition: Lemma remove_neq_mapsto_iff : forall m x y e, ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m).
proof: Proof. split; [apply remove_3|apply remove_2]; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface