diff --git a/theories/hocap/shared_bag.v b/theories/hocap/shared_bag.v
index c9911f110d4e7327796e850f8a71debede2c2b2a..cd2026606b6c664604fb99d27e233758e68d1b9a 100644
--- a/theories/hocap/shared_bag.v
+++ b/theories/hocap/shared_bag.v
@@ -52,7 +52,7 @@ Section proof.
     { iModIntro. iIntros (Y) "[Hb1 HP]".
       iInv NI as (X) "[>Hb2 HPs]" "Hcl".
       iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
-      iMod (bag_contents_update b ({[v]} ⊎ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
+      iMod (bag_contents_update b ({[+ v +]} ⊎ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
       iFrame. iApply "Hcl".
       iNext. iExists _; iFrame.
       rewrite big_sepMS_singleton. iFrame. }