diff --git a/source/vstd/hash_map.rs b/source/vstd/hash_map.rs
index 9da8271c5..9fcbc17f0 100644
--- a/source/vstd/hash_map.rs
+++ b/source/vstd/hash_map.rs
@@ -110,6 +110,14 @@ impl<Key, Value> HashMapWithView<Key, Value> where Key: View + Eq + Hash {
     {
         self.m.clear()
     }
+
+    #[verifier::external_body]
+    pub fn union_prefer_right(&mut self, other: Self)
+        ensures
+            self@ == old(self)@.union_prefer_right(other@),
+    {
+        self.m.extend(other.m)
+    }
 }
 
 pub broadcast proof fn axiom_hash_map_with_view_spec_len<Key, Value>(
@@ -211,6 +219,14 @@ impl<Value> StringHashMap<Value> {
     {
         self.m.clear()
     }
+
+    #[verifier::external_body]
+    pub fn union_prefer_right(&mut self, other: Self)
+        ensures
+            self@ == old(self)@.union_prefer_right(other@),
+    {
+        self.m.extend(other.m)
+    }
 }
 
 pub broadcast proof fn axiom_string_hash_map_spec_len<Value>(m: &StringHashMap<Value>)