proposition: Lemma remove_2 : forall m (Hm:Sort m) x y e, ~ X.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
proof: Proof. intros m Hm x y e He H. induction Hm as [|[a m] l Hm IHHm Hr]; simpl in *. - now inversion H. - destruct X.compare as [Hlt|Heq|Hgt]. + assumption. + apply InA_cons in H; destruct H; [compute in H; destruct H; order|]. apply H. + apply InA_cons in H; destruct H. * apply InA_cons_hd; assumption. * apply InA_cons_tl, IHHm, H. Qed.
imports: FMapInterface