diff --git a/Source/DafnyCore/DafnyPrelude.bpl b/Source/DafnyCore/DafnyPrelude.bpl
index 614018ead48..579eede1e33 100644
--- a/Source/DafnyCore/DafnyPrelude.bpl
+++ b/Source/DafnyCore/DafnyPrelude.bpl
@@ -1207,13 +1207,13 @@ axiom (forall<U, V> m: Map U V ::
   m == Map#Empty() || (exists k, v: Box :: Map#Items(m)[$Box(#_System._tuple#2._#Make2(k, v))]));
 
 axiom (forall<U, V> m: Map U V ::
-  { Set#Card(Map#Domain(m)) }
+  { Set#Card(Map#Domain(m)) } { Map#Card(m) }
   Set#Card(Map#Domain(m)) == Map#Card(m));
 axiom (forall<U, V> m: Map U V ::
-  { Set#Card(Map#Values(m)) }
+  { Set#Card(Map#Values(m)) } { Map#Card(m) }
   Set#Card(Map#Values(m)) <= Map#Card(m));
 axiom (forall<U, V> m: Map U V ::
-  { Set#Card(Map#Items(m)) }
+  { Set#Card(Map#Items(m)) } { Map#Card(m) }
   Set#Card(Map#Items(m)) == Map#Card(m));
 
 // The set of Values of a Map can be obtained by the function Map#Values, which is
diff --git a/Test/git-issues/git-issue-2380.dfy b/Test/git-issues/git-issue-2380.dfy
new file mode 100644
index 00000000000..3d024d29c20
--- /dev/null
+++ b/Test/git-issues/git-issue-2380.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M0(t: map<int, int>, k: int)
+  requires k in t
+{
+  if * {
+    assert |t| == |t - {k}| + 1;
+  } else if * {
+    assume t.Items == {(1, 2), (3, 4)};
+    assert |t| == 2;
+  } else {
+    assume t.Values == {2, 3, 4};
+    assert |t| >= 2;
+  }
+}
+
+method M0'(t: map<int, int>, k: int)
+  requires k in t
+{
+  if * {
+    var _ := |(t - {k}).Keys|;
+    assert |t| == |t - {k}| + 1;
+  } else if * {
+    assume t.Items == {(1, 2), (3, 4)};
+    var _ := |t.Items|;
+    assert |t| == 2;
+  } else {
+    assume t.Values == {2, 3, 4};
+    assert |t.Values| >= 2;
+  }
+}
diff --git a/Test/git-issues/git-issue-2380.dfy.expect b/Test/git-issues/git-issue-2380.dfy.expect
new file mode 100644
index 00000000000..ebe2328e072
--- /dev/null
+++ b/Test/git-issues/git-issue-2380.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors