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; apply Raw.add_3; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses