diff --git a/opam b/opam
index c99b251dc128b90232b54c448b41242ad655a27f..96e5496c252c6ddc7fc6f0f5c86c1500eb533a70 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-07-19.3.ce8bd0c6") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-07-26.8.eb05e835") | (= "dev") }
 ]
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 62d5dfced188bed808c39c36eea6326dc328675c..8f0f97cfa561d326e4bc10d52b683cba5f8da3d8 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -160,7 +160,7 @@ Section mapper.
       iIntros (ys'). iDestruct 1 as (Hys) "Hcsort"; simplify_eq/=.
       rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
       iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
-        -?gmultiset_elem_of_singleton_subseteq //.
+        ?gmultiset_singleton_subseteq_l //.
       rewrite (comm_L disj_union) gmultiset_elements_disj_union.
       by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L comm.
   Qed.
@@ -266,7 +266,7 @@ Section mapper.
       iIntros (zs'); iDestruct 1 as (Hzs) "HIC"; simplify_eq/=.
       iApply ("HΦ" $! (zs' ++ red i ys)). iSplit; last by rewrite -assoc_L.
       iPureIntro. rewrite (gmultiset_disj_union_difference {[+ (i,ys) +]} Y)
-        -?gmultiset_elem_of_singleton_subseteq //.
+        ?gmultiset_singleton_subseteq_l //.
       rewrite (comm_L disj_union) gmultiset_elements_disj_union.
       rewrite gmultiset_elements_singleton assoc_L Hzs !bind_app /=.
       by rewrite right_id_L !assoc_L.
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index a4cd7c779d59ffd245ba2629a358ae7cecde9dfc..d9f6f80418e3442e90ad5b89a540240dd42992b1 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -187,7 +187,7 @@ Section map.
       iIntros (ys'); iDestruct 1 as (Hys) "Hk"; simplify_eq/=.
       iApply ("HΦ" $! (ys' ++ map x)). iSplit.
       + iPureIntro. rewrite (gmultiset_disj_union_difference {[+ x +]} X)
-          -?gmultiset_elem_of_singleton_subseteq //.
+          ?gmultiset_singleton_subseteq_l //.
         rewrite (comm_L disj_union) gmultiset_elements_disj_union.
         by rewrite gmultiset_elements_singleton assoc_L bind_app -Hys /= right_id_L.
       + by rewrite -assoc_L.