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