proposition: Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
proof: Proof. intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses