proposition: Lemma remove_3 : forall m (Hm:NoDupA m) x y e, MapsTo y e (remove x m) -> MapsTo y e m.
proof: Proof. induction m as [|[a m]]; intros Hm x y e H; unfold PX.MapsTo; simpl in *; auto. destruct X.eq_dec. - apply InA_cons_tl; apply H. - inversion_clear Hm; apply InA_cons in H; destruct H; [apply InA_cons_hd; auto|]. apply InA_cons_tl; apply IHm with x; auto. Qed.
imports: FMapInterface