proposition: Lemma remove_2 : forall m (Hm:NoDupA m) x y e, ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
proof: Proof. induction m as [|[a m]]; intros Hm x y e H He; simpl in *. + inversion_clear He. + apply InA_cons in He; destruct He, X.eq_dec. - elim H; apply X.eq_trans with a; [auto|]; apply X.eq_sym; apply H0. - inversion_clear Hm; apply InA_cons_hd; assumption. - apply H0. - inversion_clear Hm. apply InA_cons; destruct (X.eq_dec y a). * elim H1; apply InA_eqk with (y, e); [assumption|]; apply InA_eqke_eqk; auto. * right; apply IHm; auto. Qed.
imports: FMapInterface