proposition: Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m).
proof: Proof. intros; unfold map. destruct (mapi_1 (fun _ => f) H); intuition. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface