proposition: Lemma add_1 : forall m x y e, eq x y -> MapsTo y e (add x e m).
proof: Proof. intros m x y e; generalize y; clear y. unfold MapsTo. functional induction (add x e m);simpl;auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses