proposition: Lemma add_2 : forall m x y e e', ~ eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
proof: Proof. intros m x y e e'. generalize y e; clear y e; unfold MapsTo. functional induction (add x e' m) ;simpl;auto; clear e0. subst;auto. intros y' e'' eqky'; inversion_clear 1; destruct H0; simpl in *. subst. now contradict eqky'. auto. auto. intros y' e'' eqky'; inversion_clear 1; intuition. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses