proposition: Lemma add_3 : forall m x y e e', ~ eq x y -> MapsTo y e (add x e' m) -> MapsTo y 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; intros. apply (In_inv_3 H0); compute; auto. apply (In_inv_3 H0); compute; auto. constructor 2; apply (In_inv_3 H0); compute; auto. inversion_clear H0; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses