diff --git a/opam b/opam
index da9c8699bb98aa1a7a23c3bf78232ae83b330127..588720cffff431c25131578c272a38e6936c51a5 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/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-05-29.3.54efc60b") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-06-10.4.237fd8c7") | (= "dev") }
 ]
diff --git a/theories/escrows.v b/theories/escrows.v
index 3bf228337c2a82e655477424ed6f33e1bbda20f7..9e263e0d9785ef76ecfc11bf05054f910cd6d193 100644
--- a/theories/escrows.v
+++ b/theories/escrows.v
@@ -84,7 +84,8 @@ Section proof.
     iAssert (▷ (Q V ∗ (P V ∨ Q V)))%I with "[P Inv ND]" as "[Q Inv]".
       { iNext.
         iDestruct "Inv" as "[Inv|$]".
-        - iExFalso. iApply ("ND" $! V0 with "[%//] [$P $Inv]").
+        - iExFalso. setoid_rewrite monPred_at_impl.
+          iApply ("ND" $! V0 with "[%//] [$P $Inv]").
         - by iLeft. }
     by iMod ("HClose" with "Inv").
   Qed.
@@ -135,6 +136,7 @@ Section proof.
         - iExFalso.
           iDestruct "oP" as (V1) "P1".
           iDestruct "Inv" as (V2) "P2".
+          setoid_rewrite monPred_at_impl.
           iApply ("ND" $! (V1 ⊔ V2 ⊔ V0) with "[%] [$P1 $P2]"). solve_jsl.
         - iLeft. iDestruct "oP" as (?) "oP". by iExists _.  }
     iMod ("HClose" with "Inv"). auto.
diff --git a/theories/gps/cas.v b/theories/gps/cas.v
index 0d4db7335d7515e69f900b68f0c20852c125bcae..db351cfaab37b46d0ec9d3f5ff00f470d5ccb864 100644
--- a/theories/gps/cas.v
+++ b/theories/gps/cas.v
@@ -101,7 +101,7 @@ Section CAS.
               + exists t. by rewrite -Eq -Eq1. }
 
         rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
-        iDestruct "oBEI" as "[F oBEI]".
+        iDestruct "oBEI" as "[F oBEI]". setoid_rewrite monPred_at_wand.
         iMod ("VS1" $! _ V' with "[//] [$F $P //]") as (s'') "(% & T & oW)".
 
         iDestruct "oW" as (ζ') "oW".
@@ -250,6 +250,7 @@ Section CAS.
       (* Case: CAS fails *)
       + rewrite /All_Inv (big_sepS_delete _ _ _ InVr).
         iDestruct "oAI" as "[Fp oAI]".
+        setoid_rewrite monPred_at_wand.
         iMod ("VSDup" $! s' v Vr with "[//] [$Fp //]") as "[Fp Fp']".
         iCombine "Fp'" "oAI" as "oAI". rewrite -(big_sepS_delete _ _ _ InVr).
         iMod (Reader_fork_Auth_2 _ _ {[s', (v, Vr)]} with "[$oA]") as "[oA #oR']".
@@ -307,13 +308,16 @@ Section CAS.
       iFrame "VSDup P".
       iSplitL "VS"; last iSplitR "VSF oW"; last iSplitR "oW"; last done; iNext.
       - iIntros (s' V1 VV1) "(Hsr & F & P & oW)".
+        setoid_rewrite monPred_at_wand.
         iMod ("VS" $! s' V1 with "[//] [$F $P $Hsr]") as (s'') "?".
-        iExists s''. by iFrame.
+        iExists s''. setoid_rewrite monPred_at_wand. by iFrame.
       - iIntros (? ? ?) "_ (_ & _ & (? & ? & Q) & ?)".
         iModIntro; iFrame.
         iIntros (?? HV) "(? & ? & ? & ? & ?)".
+        setoid_rewrite monPred_at_wand.
         iApply ("Q" $! _ _ with "[//] [-]"). iFrame.
       - iIntros (???? HV) "(? & ? & ? & (? & ?) & ? & ? & ? & ? & ?)".
+        setoid_rewrite monPred_at_wand.
         iApply ("VSF" $! _ _ _ _ with "[//] [-]"). iFrame. }
     iNext.
     iIntros (s'' b v Vr V') "(VV' & kS' & Hs'' & IF & oR' & VrV & VVr)".
diff --git a/theories/gps/fai.v b/theories/gps/fai.v
index f0a54646af6b8540195eb6f20414d0528554ade7..2654001195760ab1cfd2bda486702f89c36727cf 100644
--- a/theories/gps/fai.v
+++ b/theories/gps/fai.v
@@ -90,6 +90,7 @@ Section FAI.
       rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
       iDestruct "oBEI" as "[F oBEI]".
 
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! v s' V' with "[//] [$F $P //]") as (s'') "(% & Q & F & Fp)".
 
       iDestruct "oW" as (ζ') "oW".
diff --git a/theories/gps/fractional.v b/theories/gps/fractional.v
index adb3e7d5c72318f0edde10627405bb1b5bd95757..0c2e12b317fa43cfd887220c7db2506c561d44c7 100644
--- a/theories/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -116,6 +116,7 @@ Section Fractional.
       - iExists {[s, (v, V')]}. iFrame "oI oW". by iNext.
       - iExists (s, (v, V')). iFrame "ex". iSplitL ""; first done.
         iExists V', v. iFrame "oR". rewrite monPred_in_eq /=. by iSplit. }
+    setoid_rewrite monPred_at_wand.
     iModIntro; iApply ("Post" $! _ with "[%]").
     { etrans; eauto. }
     rewrite vGPS_FP_eq /=; done.
@@ -161,15 +162,16 @@ Section Fractional.
           iExists Vr, v. rewrite monPred_in_eq /=.
           iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
+      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
       iMod ("VS" $! _ j0 with "[% ] [$]") as "$".
       { repeat (etrans; eauto). }
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
-    iFrame.
+    iFrame. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    by iFrame "Hs'".
+    setoid_rewrite monPred_at_sep. by iFrame "Hs'".
   Qed.
 
   Lemma GPS_FP_Read l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -229,13 +231,14 @@ Section Fractional.
         + iNext. iExists γ, γ_x, ζ. iFrame; auto.
         + iExists γ, γ_x, e_x. iFrame "Hex". iSplitL ""; first auto.
           iExists V_r, v_r. rewrite monPred_in_eq /=; auto. }
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ j0 with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V'') "(% & kS' & #Hs' & oQ & #oR' & % & %)".
-    iFrame.
+    iFrame. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! _ _ _ with "[%]"); [solve_jsl|].
-    by iFrame "Hs'".
+    setoid_rewrite monPred_at_sep. by iFrame "Hs'".
   Qed.
 
   Lemma GPS_FP_Read_abs l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -287,6 +290,7 @@ Section Fractional.
     [solve_ndisj|auto|auto|auto|..].
     iNext.
     iIntros (V') "(% & kS' & oI & ex & #oR' & wTok)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ with "[%]").
     { etrans; eauto. }
     iAssert (monPred_at (vGPS_FP l s' q) V') with "[HT ex]" as "oW".
@@ -299,7 +303,7 @@ Section Fractional.
     }
     assert (V ⊑ V') by (do 2 (etrans; eauto)).
     iMod ("VS" $! _ with "[%] [oP oW]") as "($ & oF & oFp)"; first done.
-    { rewrite vGPS_FP_eq /=; iFrame. }
+    { rewrite monPred_at_sep. rewrite vGPS_FP_eq /=; iFrame. }
     iSpecialize ("oI" with "[$oF $oFp]").
     iMod ("HClose" with "[-]") as "$"; [|done].
     iNext. iExists γ, γ_x, ({[s', (v, V')]} ∪ ζ).
@@ -341,15 +345,16 @@ Section Fractional.
     { etrans; eauto. }
     { iSplitR "wTok"; last by iExists _.
       iNext.
-      iIntros (?? j ?) "Hs'".
+      iIntros (?? j ?) "Hs'". setoid_rewrite monPred_at_wand.
       iApply ("VS" $! _ _ _ with "[%] [-//]").
       etrans; eauto. }
     iNext.
     iIntros (s'' v Vr V')
             "(% & kS' & Hs' & oI & Q & ex & #oR' & % & % & wTok)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    iFrame "Hs' Q".
+    rewrite monPred_at_sep. iFrame "Hs' Q".
     iApply "HClose". iSplitL "oI wTok".
     - iNext. iDestruct "wTok" as (ζ') "wTok".
       iExists γ, γ_x, _.
@@ -400,6 +405,7 @@ Section Fractional.
       [solve_ndisj|solve_ndisj|solve_ndisj| |].
     { iSplitL "VS"; last iSplitL "VSDup"; last iSplitL "VSF"; last (by iFrame; iExists _); iNext.
       - iIntros (s' j ?) "(Hs' & F & oP & HClose)".
+        setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
         iMod ("VS" $! _ _ with "[%] [$Hs' $F $oP]") as (s'') "(? & ? & ? & Q)".
         { etrans; eauto. }
         iExists s''; iFrame.
@@ -412,6 +418,7 @@ Section Fractional.
             iExists Vr, v_n. rewrite monPred_in_eq /=.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
+        setoid_rewrite monPred_at_wand.
         iMod ("Q" $! j0 with "[//] [$oW]") as "$".
         iApply fupd_intro_mask'. solve_ndisj.
       - by iSpecialize ("VSDup" $! _).
@@ -424,6 +431,8 @@ Section Fractional.
             iExists Vr, v. rewrite monPred_in_eq /=.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
+        setoid_rewrite monPred_at_wand. do 4 setoid_rewrite monPred_at_sep.
+        setoid_rewrite monPred_at_later.
         iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
         { etrans; eauto. }
         iApply fupd_intro_mask'. solve_ndisj. }
@@ -431,10 +440,10 @@ Section Fractional.
     iNext.
     iIntros (s'' b v Vr V')
             "(% & kS' & Hs' & IF & #oR' & % & %)".
-    iFrame.
+    iFrame. setoid_rewrite monPred_at_wand.
     iSpecialize ("Post" $! s'' b v _ with "[%]").
     { etrans; eauto. }
-    iApply "Post". iFrame "Hs'". by destruct b.
+    iApply "Post". rewrite monPred_at_sep. iFrame "Hs'". by destruct b.
   Qed.
 
   Lemma GPS_FP_CAS l q s v_o v_n (E : coPset)
diff --git a/theories/gps/plain.v b/theories/gps/plain.v
index d26ccea8d2536999507fede4a13a1bec7e7ac1ba..742a7aa4810e5ae268929f35286ba7d424aea522 100644
--- a/theories/gps/plain.v
+++ b/theories/gps/plain.v
@@ -126,6 +126,7 @@ Section Plain.
       { iFrame "kI Info oI oW ex oEx".
         repeat iExists _. iFrame "oEx". iSplitL; [done|].
         iExists _, _; iFrame "oR". by iSplit. }
+      setoid_rewrite monPred_at_wand.
       iModIntro; iApply ("Post" $! _ with "[%]").
       { etrans; eauto. }
     rewrite vGPS_PP_eq /=; done.
@@ -173,11 +174,15 @@ Section Plain.
         + iExists γ, γ_x, γx, e_x'. iFrame "Hex". iSplitL ""; first auto.
           iExists Vr, v. iSplit; last iFrame "oR'"; iPureIntro; auto.
           do 4 (etrans; eauto). }
-      iMod ("VS" $! _ j0 with "[%] [$]") as "$"; [solve_jsl|].
+      setoid_rewrite monPred_at_wand.
+      iMod ("VS" $! _ j0 with "[%] [-]") as "$"; [solve_jsl|..].
+      { iFrame. done. }
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & % & oQ & #oR' & % & %)".
-    iFrame. iApply ("Post" $! s' _ _ with "[//]"). by iFrame "%".
+    iFrame. setoid_rewrite monPred_at_wand. setoid_rewrite monPred_at_sep.
+    iApply ("Post" $! s' _ _). { iPureIntro. by etrans. }
+    by iFrame "%".
   Qed.
 
   Lemma GPS_PP_Read l p (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -232,7 +237,7 @@ Section Plain.
     { do 2 (etransitivity; eauto). }
     iNext.
     iIntros (V') "(% & kS' & oI & ex & #oR' & wTok)".
-    iFrame.
+    iFrame. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! _ with "[%]").
     { etrans; eauto. }
     iAssert (persisted l (gpsPRaw p) (RPRaw p s' V')) with "[#]" as "#oPP".
@@ -292,6 +297,7 @@ Section Plain.
       [solve_ndisj|solve_ndisj|solve_ndisj| |].
     { iSplitL "VS"; last iSplitL "VSDup"; last iSplitL "VSF"; last (by iFrame; iExists _); iNext.
       - iIntros (s' j ?) "(Hs' & F & oP & HClose)".
+        setoid_rewrite monPred_at_wand. setoid_rewrite monPred_at_sep.
         iMod ("VS" $! _ _ with "[%] [$Hs' $F $oP]") as (s'') "(? & ? & ? & Q)".
         { etrans; eauto. }
         iExists s''; iFrame.
@@ -304,6 +310,7 @@ Section Plain.
             iExists Vr, v_n.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
+        setoid_rewrite monPred_at_wand.
         iMod ("Q" $! _ with "[//] [oW //]") as "$".
         iApply fupd_intro_mask'. solve_ndisj.
       - by iSpecialize ("VSDup" $! _).
@@ -316,6 +323,8 @@ Section Plain.
             iExists Vr, v.
             iSplit; last iFrame "oR'"; iPureIntro; auto.
             do 4 (etrans; eauto). }
+        setoid_rewrite monPred_at_wand. do 4 setoid_rewrite monPred_at_sep.
+        setoid_rewrite monPred_at_later.
         iMod ("VSF" $! _ _ _ with "[%] [$Hs' $Hv $Fp $oW $oP]") as "$".
         { etrans; eauto. }
         iApply fupd_intro_mask'. solve_ndisj. }
@@ -323,10 +332,10 @@ Section Plain.
     iNext.
     iIntros (s'' b v Vr V')
             "(% & kS' & Hs' & IF & #oR' & % & %)".
-    iFrame.
+    iFrame. setoid_rewrite monPred_at_wand.
     iSpecialize ("Post" $! s'' b v _ with "[%]").
     { etrans; eauto. }
-    iApply "Post". iFrame. by destruct b.
+    iApply "Post". rewrite monPred_at_sep. iFrame. by destruct b.
   Qed.
 
   Lemma GPS_PP_CAS l p s v_o v_n (E : coPset)
@@ -396,10 +405,12 @@ Section Plain.
     { etrans; eauto. }
     { iSplitR "wTok"; last by iExists _.
       iNext; iIntros (?? j ?) "?".
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ _ j with "[%] [-//]"); [solve_jsl|done]. }
     iNext.
     iIntros (s'' v Vr V')
             "(% & kS' & Hs' & oI & Q & ex & #oR' & % & % & wTok)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); [solve_jsl|].
     iFrame.
     iApply "HClose". iSplitL "oI ex wTok".
diff --git a/theories/gps/read.v b/theories/gps/read.v
index a6fe307616f661489efbdf38d7efdcc997735c30..8db2b960af1b2b4c05e860468ec601bb1ed5db06 100644
--- a/theories/gps/read.v
+++ b/theories/gps/read.v
@@ -71,6 +71,7 @@ Section Read.
       iDestruct ("VS" $! s' with "[//]") as "[VS|VS]".
       + rewrite /All_Inv (big_sepS_delete _ _ _ In).
         iDestruct "oAI" as "[Fp oAI]".
+        setoid_rewrite monPred_at_wand.
         iMod ("VSDup" $! _ _ Vr with "[//] [$Fp //]") as "[Fp Fp']".
         iCombine "Fp'" "oAI" as "oAI".
         rewrite -(big_sepS_delete _ _ _ In).
@@ -108,6 +109,9 @@ Section Read.
 
         rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
         iDestruct "oBEI" as "[F oBEI]".
+        setoid_rewrite bi.pure_impl_forall.
+        setoid_rewrite monPred_at_forall.
+        setoid_rewrite monPred_at_wand at 2.
         iMod ("VS" $! (st_prst e) (st_val e) Hse (V ⊔ (st_view e))
              with "[%] [$F $P]") as "[]". solve_jsl.
   Qed.
@@ -146,6 +150,7 @@ Section Read.
       iDestruct "Pure" as (V'') "(% & % & %)".
       rewrite /All_Inv (big_sepS_delete _ _ _ H6).
       iDestruct "oAI" as "[Fp oAI]".
+      setoid_rewrite monPred_at_wand.
       iMod ("VSDup" $! v V with "[//] [$Fp]") as "[Fp Fp']".
       iCombine "Fp'" "oAI" as "oAI". rewrite -(big_sepS_delete _ _ _ H6).
 
diff --git a/theories/gps/singlewriter.v b/theories/gps/singlewriter.v
index fde8c74be08951babd18254e675dbfc5cc8ed8d5..67b18c6165c8a0649bf9fb3c5afa8436ba76cb61 100644
--- a/theories/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -111,6 +111,7 @@ Section Gname_StrongSW.
           iExists v, V', {[(s γ), (v, V')]}. iFrame "ex oW oR".
           iSplit; first auto. iPureIntro.
           by move => ? /elem_of_singleton ->. }
+    setoid_rewrite monPred_at_wand.
     iFrame; by iApply ("Post" $! _ V' with "[%] [$Q $FP]").
   Qed.
 
@@ -139,6 +140,7 @@ Section Gname_StrongSW.
     { iNext. by iSpecialize ("VSDup" $! _ with ""). }
     iNext.
     iIntros (v V') "(% & kS & oI & Fp & ex & oR' & wTok)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ V' with "[%]").
     { etrans; eauto. }
     iFrame "Fp".
@@ -342,6 +344,7 @@ Section Gname_StrongSW.
     iNext.
     iIntros (V') "(% & kS' & oI & oF & ex & #oR' & wTok & #Max)".
     assert (V1 ⊑ V') by (etrans; eauto).
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! V' with "[%]"); first done.
     assert (V ⊑ V') by (etrans; eauto).
     iMod ("VS" $! _ V' with "[%] [$oP $oF]") as "(oQ & oF & oFp)"; first done.
@@ -411,11 +414,13 @@ Section Gname_StrongSW.
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
+      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; first solve_jsl.
       iApply fupd_intro_mask'. solve_ndisj. }
     iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]"); first done.
-    by iFrame "Hs'".
+    rewrite monPred_at_sep. by iFrame "Hs'".
   Qed.
 
   Lemma GPS_nFRP_Read l γ q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -479,13 +484,18 @@ Section Gname_StrongSW.
           { iSplitL "oI".
             + iNext. iExists γ_x. iFrame; auto.
             + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
+          setoid_rewrite monPred_at_wand.
           iMod ("VS" $! _ _ with "[%] [-]") as "$"; first solve_jsl.
           { iFrame. }
           iApply fupd_intro_mask'. solve_ndisj.
         - iIntros "!>" (s' v ??) "[% Fp]".
+          rewrite monPred_at_objectively.
+          do 2 setoid_rewrite monPred_at_forall.
+          setoid_rewrite monPred_at_wand.
           iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
           iPureIntro. split; [by etrans|auto]. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
+      setoid_rewrite monPred_at_wand.
       iFrame; iApply ("Post" $! s' _ V'' with "[%]"); [solve_jsl|].
       iMod "Q" as "$".
       iPureIntro; split; [by etrans|auto].
@@ -500,13 +510,18 @@ Section Gname_StrongSW.
           { iSplitL "oI".
             + iNext. iExists γ_x. iFrame; auto.
             + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR1". }
+          setoid_rewrite monPred_at_wand.
           iMod ("VS" $! _ _ with "[%] [-]") as "$"; first solve_jsl.
           { iFrame. }
           iApply fupd_intro_mask'. solve_ndisj.
         - iIntros "!>" (s' v ??) "[% Fp]".
+          rewrite monPred_at_objectively.
+          do 2 setoid_rewrite monPred_at_forall.
+          setoid_rewrite monPred_at_wand.
           iApply ("VSDup" $! _ s' v _ with "[%] [$Fp]"); first reflexivity.
           iPureIntro. split; solve_jsl. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
+      setoid_rewrite monPred_at_wand.
       iFrame; iApply ("Post" $! _ _ V'' with "[%]").
       { solve_jsl. }
       iMod "Q"; iFrame.
@@ -570,10 +585,12 @@ Section Gname_StrongSW.
       { iSplitL "oI".
         + iNext. iExists γ_x. iFrame; auto.
         + iExists γ_x. iSplit; first done. iExists V1, v1. by iFrame "oR". }
+      setoid_rewrite monPred_at_wand.
       iMod ("VS" $! _ _ with "[%] [-]") as "$"; first solve_jsl.
       { iFrame. }
       iApply fupd_intro_mask'. solve_ndisj. }
       iNext. iIntros (s' v Vr V'') "(% & kS & % & Q & oR' & % & %)".
+      setoid_rewrite monPred_at_wand.
       iFrame; iApply ("Post" $! _ _ V'' with "[%]"). { solve_jsl. }
       iMod "Q"; iFrame; auto.
   Qed.
@@ -706,6 +723,7 @@ Section Gname_StrongSW_Param.
     iMod (persistor_inv_alloc' E i (encode (p,γ,γ_x)) l
           (gpsSWpnRaw p γ) (λ l X, WriterSWpnRaw p γ (s γ) l X V')
           with "[$Info $kI $kIp]") as "[WP HClose]"; [auto|auto|..].
+    setoid_rewrite monPred_at_wand.
     iMod ("VS" $! γ _ with "Le [- Post HClose oI kS]") as "(F & Fp & Q)".
     { iApply "WP".
       iExists γ_x. iSplitL ""; first done.
@@ -743,6 +761,7 @@ Section Gname_StrongSW_Param.
     iNext.
     iIntros (V') "(% & kS' & oI & oF & ex & #oR' & wTok & #?)".
     setoid_rewrite H1; setoid_rewrite H2; setoid_rewrite H4.
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! V' with "[%]"); [done|].
     iMod ("VS" $! _ _ with "[%] [$oP $oF wTok ex]") as "(oQ & oF & oFp)"; [done|..].
     - iApply "HT".
@@ -782,6 +801,7 @@ Section Gname_StrongSW_Param.
     iNext.
     iIntros (v V') "{oR} (% & kS & oI & Fp & ex & #oR' & wTok)".
     assert (V1 ⊑ V') by (etrans; eauto).
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ V' with "[%]"); first done.
     iFrame "Fp".
     iApply "HClose". iSplitL "oI".
@@ -826,11 +846,14 @@ Section Gname_StrongSW_Param.
       { iSplit.
         + iNext. iExists γ_x. by iFrame "oI".
         + iExists γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
+      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iNext.
     iIntros (s' v Vr V') "(% & kS' & Hs' & >oQ & oR' & % & %)".
-    iFrame; iApply ("Post" $! _ _ _ with "[%]"); [solve_jsl|auto].
+    setoid_rewrite monPred_at_wand.
+    iFrame; iApply ("Post" $! _ _ _ with "[%]"); first solve_jsl.
+    rewrite monPred_at_sep. auto.
   Qed.
 
   Lemma GPS_nSW_Read l γ p (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -1110,6 +1133,7 @@ Section SingleWriter.
     iNext.
     iIntros (v V') "{oR} (% & kS & oI & Fp & ex & #oR' & wTok)".
     assert (V1 ⊑ V') by (etrans; eauto).
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ V' with "[%]"); first done.
     iFrame "Fp".
     iApply "HClose". iSplitL "oI".
@@ -1141,6 +1165,7 @@ Section SingleWriter.
     iMod (persistor_inv_alloc' E i (encode (γ,γ_x)) l
           gpsSWRaw (λ l X, WriterSWRaw s l X V')
           with "[$Info $kI $kIp]") as "[WP HClose]"; [auto|auto|..].
+    setoid_rewrite monPred_at_wand.
     iMod ("VS" $! _ with "Le [- Post HClose oI kS]") as "(F & Fp & Q)".
     { iApply "WP".
       iExists γ, γ_x. iSplitL ""; first done.
@@ -1187,12 +1212,14 @@ Section SingleWriter.
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
+      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    by iFrame "Hs'".
+    rewrite monPred_at_sep. by iFrame "Hs'".
   Qed.
 
   Lemma GPS_SW_Read l (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -1243,6 +1270,7 @@ Section SingleWriter.
     iNext.
     iIntros (V') "(% & kS' & oI & oF & ex & #oR' & wTok & #?)".
     setoid_rewrite H1; setoid_rewrite H2; setoid_rewrite H4.
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! V' with "[%]"); [done|].
     iMod ("VS" $! _ _ with "[%] [$oP $oF wTok ex]") as "(oQ & oF & oFp)"; [done|..].
     - iApply "HT".
@@ -1329,6 +1357,7 @@ Section SingleWriter.
           iExists v, V', {[s, (v, V')]}. iFrame "ex oW oR".
           iSplit; first auto. iPureIntro.
           by move => ? /elem_of_singleton ->. }
+    setoid_rewrite monPred_at_wand.
     by iFrame; iApply ("Post" $! V' with "Le [$FP]").
   Qed.
 
@@ -1367,12 +1396,14 @@ Section SingleWriter.
       { iSplit.
         + iNext. iExists γ, γ_x. by iFrame "oI".
         + iExists γ, γ_x. iSplit; first done. iExists Vr, v. by iFrame "oR'". }
+      setoid_rewrite monPred_at_wand. do 2 setoid_rewrite monPred_at_sep.
       iMod ("VS" $! _ _ with "[%] [$]") as "$"; [solve_jsl|].
       iApply fupd_intro_mask'. solve_ndisj. }
     iIntros "!>" (s' v Vr V') "(% & kS' & Hs' & oQ & oR' & % & %)".
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ _ _ with "[%]").
     { etrans; eauto. }
-    by iFrame "Hs'".
+    rewrite monPred_at_sep. by iFrame "Hs'".
   Qed.
 
   Lemma GPS_FRP_Read l q (P : vPred) (Q : pr_state Prtcl → Z → vPred)
@@ -1421,6 +1452,7 @@ Section SingleWriter.
     iNext.
     iIntros (v V') "(% & kS & oI & Fp & ex & oR' & wTok)".
     assert (V1 ⊑ V') by (etrans; eauto).
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! _ V' with "[%]"); first done.
     iFrame "Fp".
     iApply "HClose". iSplitL "oI".
@@ -1563,6 +1595,7 @@ Section SingleWriter.
     iNext.
     iIntros (V') "(% & kS' & oI & oF & ex & #oR' & wTok & #Max)".
     setoid_rewrite H1; setoid_rewrite H2; setoid_rewrite H4.
+    setoid_rewrite monPred_at_wand.
     iFrame; iApply ("Post" $! V' with "[%]"); [done|].
     iMod ("VS" $! _ _ with "[%] [$oP $oF]") as "(oQ & oF & oFp)"; [done|..].
     iFrame "oQ". iApply ("HClose"). iSplitL "oI oF oFp".
diff --git a/theories/malloc.v b/theories/malloc.v
index 62faeacac9ffc9e4a5d023e77c75b4939a1d3e08..ae904f9a29e334b89f4345324532692f312e4563 100644
--- a/theories/malloc.v
+++ b/theories/malloc.v
@@ -54,7 +54,7 @@ Section proof.
     last (iApply (f_alloc with "[$kI $kS]"));
     first auto.
     iNext. iIntros (l V' h' i) "(% & $ & oH & oI & % & % & %)".
-    destruct H2; subst.
+    destruct H2; subst. setoid_rewrite monPred_at_wand.
     iApply ("Post" $! _ _ with "[%]"); [etrans;done|].
     iExists _, _. by iFrame "oH oI".
   Qed.
diff --git a/theories/na.v b/theories/na.v
index b682fc4050184d6607fe2aa12f20a5de36820f99..981e05a020a72d3ed350c117d0b12d240ae10b52 100644
--- a/theories/na.v
+++ b/theories/na.v
@@ -376,6 +376,7 @@ Section FractionalRules.
     - iNext. iIntros (v_r V') "(% & $ & oH & % & H)".
       iDestruct "H" as (V_1) "(% & % & %)".
       move: H7 => /value_at_hd_singleton [[?] ?]. subst v_r V_1.
+      setoid_rewrite monPred_at_wand.
       iApply ("Post" $! _ _ with "[%]"); [by etrans|].
       iMod ("HClose" $! (λ _ _ X, ⌜X = encode (VInj v)⌝)%I with "[$oH $HX]")
         as "ol".
diff --git a/theories/rsl.v b/theories/rsl.v
index b0c375eb569666b122edad6b47bd04f1c77227c5..af4bcdd916840dd7e74406171e207e0694eb358d 100644
--- a/theories/rsl.v
+++ b/theories/rsl.v
@@ -916,8 +916,9 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
       rewrite (big_sepS_delete _ _ _ Hp').
       iDestruct "ress" as "(Hφ & ress)".
 
+      setoid_rewrite monPred_at_wand.
       iMod ("CSucc" $! V' with "[] [$P $Hφ $Hφd]") as "(Hφ & Hφd & R)";
-        first auto.
+        first by auto.
 
       iCombine "Hφd" "ressD" as "ressD".
       rewrite -(big_sepS_insert _ _ (VInj v_w, V')); last first.
@@ -950,6 +951,9 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
         * by exists (VInj v_w), V'.
 
     - iDestruct "CF" as %(? & NE & ? & ?).
+      setoid_rewrite bi.pure_impl_forall.
+      do 2 setoid_rewrite monPred_at_forall.
+      setoid_rewrite monPred_at_wand at 2.
       iMod ("CFail" $! v NE V' with "[//] [$P $Hφd]") as "R".
       rewrite -sts_op_auth_frag_up.
       iDestruct "Own" as "(Own & #Own')".