proposition: Lemma remove_mapsto : forall (elt : Type) (m : t elt) (x y : key) (e : elt), MapsTo y e (remove (elt:=elt) x m) -> (not (E.eq x y)) /\ MapsTo y e m.
proof: Proof. intros; rewrite <- remove_mapsto_iff; assumption. Qed.
imports: Coq.FSets.FMaps CertifiedExtraction.PureUtils