proposition: Lemma add_mapsto_iff : forall m x y e e', MapsTo y e' (add x e m) <-> (E.eq x y /\ e=e') \/ (~E.eq x y /\ MapsTo y e' m).
proof: Proof. intros. intuition. - destruct (eq_dec x y); [left|right]. + split; auto. symmetry; apply (MapsTo_fun (e':=e) H); auto with map. + split; auto; apply add_3 with x e; auto. - subst; auto with map. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface