proposition: Lemma remove_mapsto_iff : forall m x y e, MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m.
proof: Proof. intros. split; intros. - split. + assert (In y (remove x m)) by (exists e; auto). intro H1; apply (remove_1 H1 H0). + apply remove_3 with x; auto. - apply remove_2; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface