proposition: Lemma MapsTo_add_remove : forall {elt k} {v: elt} {m}, MapsTo k v m -> Equal m (add k v (remove k m)).
proof: Proof. intros; rewrite Equal_mapsto_iff; intros k' v'; destruct (E.eq_dec k k'); msubst; map_iff; split; intros; try assert (v = v') by eauto using MapsTo_fun; subst; map_iff; intuition; subst; eauto. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils