diff --git a/examples/Collections/Maps/Maps.dfy b/examples/Collections/Maps/Maps.dfy
new file mode 100644
index 00000000..5cac2446
--- /dev/null
+++ b/examples/Collections/Maps/Maps.dfy
@@ -0,0 +1,24 @@
+// RUN: %verify "%s"
+
+/*******************************************************************************
+ * Copyright by the contributors to the Dafny Project
+ * SPDX-License-Identifier: MIT
+ *******************************************************************************/
+
+include "../../../src/Functions.dfy"
+include "../../../src/Collections/Maps/Maps.dfy"
+
+module {:options "--function-syntax:4"} MapsExamples {
+  import Functions
+  import Maps
+
+  function ByteKeyMapToIntKeys<Y>(m: map<bv8, Y>): (m': map<int, Y>)
+  {
+    Maps.MapKeys(b => b as int, m)
+  }
+
+  function ByteValueMapToIntValues<X>(m: map<X, bv8>): (m': map<X, int>)
+  {
+    Maps.MapValues(b => b as int, m)
+  }
+}
diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
index 44c7264e..430b8ace 100644
--- a/src/Collections/Maps/Maps.dfy
+++ b/src/Collections/Maps/Maps.dfy
@@ -1,18 +1,22 @@
 // RUN: %verify "%s"
 
 /*******************************************************************************
- *  Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University, 
- *  ETH Zurich, and University of Washington
- *  SPDX-License-Identifier: BSD-2-Clause 
- * 
- *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
- *  SPDX-License-Identifier: MIT 
- *******************************************************************************/
+ * Original: Copyright 2018-2021 VMware, Inc., Microsoft Inc., Carnegie Mellon University,
+ * ETH Zurich, and University of Washington
+ * SPDX-License-Identifier: BSD-2-Clause
+ *
+ * Modifications and Extensions: Copyright by the contributors to the Dafny Project
+ * SPDX-License-Identifier: MIT
+ ******************************************************************************/
 
 include "../../Wrappers.dfy"
+include "../../Functions.dfy"
+include "../Sets/Sets.dfy"
 
 module {:options "-functionSyntax:4"} Maps {
   import opened Wrappers
+  import Functions
+  import Sets
 
   function Get<X, Y>(m: map<X, Y>, x: X): Option<Y>
   {
@@ -64,7 +68,7 @@ module {:options "-functionSyntax:4"} Maps {
   ghost predicate IsSubset<X, Y>(m: map<X, Y>, m': map<X, Y>)
   {
     && m.Keys <= m'.Keys
-    && forall x {:trigger EqualOnKey(m, m', x)}{:trigger x in m} :: x in m ==> EqualOnKey(m, m', x)
+    && forall x <- m :: m[x] == m'[x]
   }
 
   /* Union of two maps. Does not require disjoint domains; on the intersection,
@@ -93,6 +97,32 @@ module {:options "-functionSyntax:4"} Maps {
     forall x, x' {:trigger m[x], m[x']} :: x != x' && x in m && x' in m ==> m[x] != m[x']
   }
 
+  lemma LemmaSubsetIsInjective<X, Y>(small: map<X, Y>, big: map<X, Y>)
+    requires IsSubset(small, big)
+    requires Injective(big)
+    ensures Injective(small)
+  {
+    reveal Injective();
+  }
+
+  lemma LemmaInjectiveImpliesUniqueValues<X(!new), Y>(m: map<X, Y>)
+    requires Injective(m)
+    ensures |m.Keys| == |m.Values|
+  {
+    if |m| > 0 {
+      reveal Injective();
+
+      var x: X :| x in m;
+      var y := m[x];
+      var m' := Remove(m, x);
+      assert IsSubset(m', m);
+
+      assert m'.Values == m.Values - {y};
+      LemmaSubsetIsInjective(m', m);
+      LemmaInjectiveImpliesUniqueValues(m');
+    }
+  }
+
   /* Swaps map keys and values. Values are not required to be unique; no
   promises on which key is chosen on the intersection. */
   ghost function {:opaque} Invert<X, Y>(m: map<X, Y>): map<Y, X>
@@ -127,4 +157,33 @@ module {:options "-functionSyntax:4"} Maps {
     forall x, x' {:trigger m[x], m[x']} :: x in m && x' in m && start <= x <= x' ==> m[x] <= m[x']
   }
 
+  /* Maps an injective function over the keys of a map, retaining the values. */
+  function {:opaque} MapKeys<X(!new), Y, X'>(f: X --> X', m: map<X, Y>): (m': map<X', Y>)
+    reads f.reads
+    requires forall x {:trigger f.requires(x)} :: f.requires(x)
+    requires Functions.Injective(f)
+    ensures |m'| == |m|
+    ensures m'.Values == m.Values
+    ensures forall x | x in m :: f(x) in m' && (m'[f(x)] == m[x])
+  {
+    var m' := map k <- m :: f(k) := m[k];
+    Sets.LemmaMapSize(m.Keys, m'.Keys, f);
+    m'
+  }
+
+  /* Maps a function over the values of a map, retaining the keys. */
+  function {:opaque} MapValues<X, Y(!new), Y'>(f: Y --> Y', m: map<X, Y>): (m': map<X, Y'>)
+    reads f.reads
+    requires forall y {:trigger f.requires(y)} :: f.requires(y)
+    ensures |m'| == |m|
+    ensures m'.Keys == m.Keys
+    ensures forall x | x in m :: m'[x] == f(m[x])
+  {
+    var m' := map x <- m :: x := f(m[x]);
+    assert |m'| == |m| by {
+      assert m'.Keys == m.Keys;
+      assert |m'.Keys| == |m.Keys|;
+    }
+    m'
+  }
 }