diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
index b06e65cd..fe8c5c28 100644
--- a/src/Collections/Maps/Maps.dfy
+++ b/src/Collections/Maps/Maps.dfy
@@ -48,6 +48,17 @@ module Maps {
     m'
   }
 
+  /* Map a function to the values of a map */
+  function method {:opaque} mapValue<K, V, V'>(f: V -> V', m: map<K, V>): (m':map<K, V'>)
+    requires forall k:: k in m.Keys ==> f.requires(m[k])
+    ensures m.Keys == m'.Keys
+    ensures |m| == |m'|
+  {
+    var result := map k | k in m :: f(m[k]);
+    assert |result.Keys| == |result|;
+    result
+  }
+
   /* Keep all key-value pairs corresponding to the set of keys provided. */
   function method {:opaque} Restrict<X, Y>(m: map<X, Y>, xs: set<X>): (m': map<X, Y>)
     ensures m' == RemoveKeys(m, m.Keys - xs)
diff --git a/src/Collections/Maps/Maps.dfy.expect b/src/Collections/Maps/Maps.dfy.expect
index 66ffe366..4b0fec56 100644
--- a/src/Collections/Maps/Maps.dfy.expect
+++ b/src/Collections/Maps/Maps.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 14 verified, 0 errors
+Dafny program verifier finished with 15 verified, 0 errors