diff --git a/theories/examples/map.v b/theories/examples/map.v
index 76b65892ca34191801d0ca214acf9dbbd7c6bbdb..5cafc7fe16ef5ff26cb09586c7320df1583e4473 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -185,7 +185,7 @@ Section map.
       iApply ("HΦ" $! (ys' ++ map x)). iSplit.
       + iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
           -?gmultiset_elem_of_singleton_subseteq //.
-        rewrite (comm disj_union) gmultiset_elements_disj_union.
+        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.
   Qed.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 6d872ce5353679fab50daaf00627621148023e70..97f5853f82ec1547d0b05de6841fce892a278a3c 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -160,7 +160,7 @@ Section mapper.
       rewrite -assoc_L. iApply ("HΦ" $! (map x ++ ys') with "[$Hcsort]").
       iPureIntro. rewrite (gmultiset_disj_union_difference {[ x ]} X)
         -?gmultiset_elem_of_singleton_subseteq //.
-      rewrite (comm disj_union) gmultiset_elements_disj_union.
+      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.
       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 //.
-      rewrite (comm disj_union) gmultiset_elements_disj_union.
+      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.
   Qed.