proposition: Lemma MapsTo_1 : forall m x y e, eq x y -> MapsTo x e m -> MapsTo y e m.
proof: Proof. intros m. apply (Raw.MapsTo_eq key_dec elt_dec). Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses