proposition: Lemma remove_3 : forall m (Hm:Sort m) x y e, MapsTo y e (remove x m) -> MapsTo y e m.
proof: Proof. intros m Hm x y e 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_tl, H. + apply InA_cons in H; destruct H. * apply InA_cons_hd; assumption. * apply InA_cons_tl, IHHm, H. Qed.
imports: FMapInterface