diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 6b749ba8cec697fd3d3e856f752a35f7e15f6b84..79b06f6179517eea4e97fc604962eb0b8cdf233c 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-11-17.0.921e8532") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-11-26.1.04496bec") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index d6074309f10c038a965f8e04de89b3c0ba521698..4cdbd4c3d43830c3240011edf8a0b30cf02042cb 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -361,16 +361,13 @@ Section arc.
       (monPred_in Vb →
         ▷ GPS_INV (weak_interp P2 l γi γs γsw) (l >> 1) (weak_noCAS γsw) γw).
   Proof.
-    rewrite 4!bi.later_sep monPred_in_sep 3!monPred_in_sep.
+    rewrite -!view_join_unfold !view_join_later.
     iDestruct 1 as "((SMA & SDA & WUA) & $ & $)".
-    rewrite 3!bi.later_exist 3!monPred_in_exist.
-    iDestruct "SMA" as (Mt) "SMA". iDestruct "SDA" as (Dt) "SDA".
-    iDestruct "WUA" as (Ut) "WUA".
-    iMod (monPred_in_later_timeless with "SMA") as "SMA".
-    iMod (monPred_in_later_timeless with "SDA") as "SDA".
-    iMod (monPred_in_later_timeless with "WUA") as "WUA".
-    iIntros "!>". iSplitL "SMA"; last iSplitL "SDA"; iExists _;
-      by iApply monPred_in_embed.
+    iDestruct "SMA" as (Mt) ">SMA". iDestruct "SDA" as (Dt) ">SDA".
+    iDestruct "WUA" as (Ut) ">WUA".
+    iIntros "!>".
+    iSplitL "SMA"; last iSplitL "SDA"; iExists _;
+      rewrite view_join_embed; iFrame.
   Qed.
 
   Lemma arc_inv_join Vb γi γs γw γsw l :
@@ -404,17 +401,17 @@ Section arc.
   Proof.
     iIntros "HP Hacc". iMod ("Hacc" with "HP") as (Vb q) "[Hown Hclose2]".
     iExists Vb, q. iMod (monPred_in_later_timeless with "Hown") as "Hown".
-    rewrite monPred_in_exist. iDestruct "Hown" as (v) "Hown".
-    rewrite monPred_in_exist. iDestruct "Hown" as (Mt) "Hown".
-    rewrite monPred_in_exist. iDestruct "Hown" as (Dt) "Hown".
-    rewrite 7!monPred_in_sep.
+    rewrite monPred_in_exist'. iDestruct "Hown" as (v) "Hown".
+    rewrite monPred_in_exist'. iDestruct "Hown" as (Mt) "Hown".
+    rewrite monPred_in_exist'. iDestruct "Hown" as (Dt) "Hown".
+    rewrite 7!monPred_in_sep'.
     iDestruct "Hown" as "(St & tok & SR & SM & SeenM & SD & SeenD & oW)".
     iExists Mt, Dt. iFrame "tok". iSplitR "Hclose2 SeenM SeenD".
-    - iSplitL "St". { by rewrite monPred_in_embed /StrongTok. }
+    - iSplitL "St". { by rewrite monPred_in_embed' /StrongTok. }
       iSplitL "SR". { by iExists _. } iSplitL "SM".
-      { by rewrite monPred_in_embed /StrMoves. } iSplitL "SD".
-      { by rewrite monPred_in_embed /StrDowns. }
-      by rewrite monPred_in_embed.
+      { by rewrite monPred_in_embed' /StrMoves. } iSplitL "SD".
+      { by rewrite monPred_in_embed' /StrDowns. }
+      by rewrite monPred_in_embed'.
     - iIntros "!>" (Mt' Dt') "St tok SR SM SeenM' SD SeenD' oW".
       iMod ("Hclose2" with "[-]") as "$"; [|done]. iIntros "#mb !>".
       iSpecialize ("tok" with "mb").
@@ -504,12 +501,12 @@ Section arc.
   Proof.
     iIntros "HP Hacc". iMod ("Hacc" with "HP") as (Vb q) "[Hown Hclose2]".
     iExists Vb, q. iMod (monPred_in_later_timeless with "Hown") as "Hown".
-    rewrite monPred_in_exist. iDestruct "Hown" as (v) "Hown".
-    rewrite monPred_in_exist. iDestruct "Hown" as (Ut) "Hown". iExists Ut.
-    rewrite 4!monPred_in_sep. iDestruct "Hown" as "(Wt & $ & WR & WU & SeenU)".
+    rewrite monPred_in_exist'. iDestruct "Hown" as (v) "Hown".
+    rewrite monPred_in_exist'. iDestruct "Hown" as (Ut) "Hown". iExists Ut.
+    rewrite 4!monPred_in_sep'. iDestruct "Hown" as "(Wt & $ & WR & WU & SeenU)".
     iSplitR "Hclose2 SeenU".
-    - iSplitL "Wt". { by rewrite monPred_in_embed /WeakTok. }
-      iSplitL "WR". { by iExists _. } by rewrite monPred_in_embed /WkUps.
+    - iSplitL "Wt". { by rewrite monPred_in_embed' /WeakTok. }
+      iSplitL "WR". { by iExists _. } by rewrite monPred_in_embed' /WkUps.
     - iIntros "!>" (Ut') "Wt tok WR WU SeenU'".
       iMod ("Hclose2" with "[-]") as "$"; [|done]. iIntros "#mb !>".
       iDestruct "WR" as (v') "WR". iSpecialize ("WR" with "mb").
@@ -715,7 +712,7 @@ Section arc.
     iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _  q
         with "RR [SR]") as "[SR1 SR2]".
     { rewrite monPred_subjectively_unfold.
-      iDestruct (monPred_in_elim_vProp with "SR") as (V') "SR". by iExists V'. }
+      iDestruct (monPred_in_view_elim with "SR") as (V') "SR". by iExists V'. }
     set R : time → unitProtocol → val → vProp :=
       (λ t' _ v', (∃ z : Z, ⌜v' = #z ∧ 0 < z⌝) ∗
             StrongTok γsw q ∗ StrongMoveAuth γsw Mt )%I.
@@ -830,7 +827,7 @@ Section arc.
     iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _  q
         with "RR [SR]") as "[SR1 SR2]".
     { rewrite monPred_subjectively_unfold.
-      iDestruct (monPred_in_elim_vProp with "SR") as (V') "SR". by iExists V'. }
+      iDestruct (monPred_in_view_elim with "SR") as (V') "SR". by iExists V'. }
     set R : time → unitProtocol → val → vProp := (λ t' _ v', ∃ z : Z, ⌜v' = #z⌝)%I.
     (* actual read *)
     iApply (GPS_SWRaw_SharedReader_Read (strong_interp P1 (l >> 1) γi γw γsw) _
@@ -869,7 +866,7 @@ Section arc.
     iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _  q
         with "RR [SR]") as "[SR1 SR2]".
     { rewrite monPred_subjectively_unfold.
-      iDestruct (monPred_in_elim_vProp with "SR") as (V') "SR". by iExists V'. }
+      iDestruct (monPred_in_view_elim with "SR") as (V') "SR". by iExists V'. }
     iDestruct "SMA" as (Mt') "SMA".
     iDestruct (StrongMoveAuth_agree with "[$SMA $SM]") as %?. subst Mt'.
     set Q: time → unitProtocol → vProp :=
@@ -1256,7 +1253,7 @@ Section arc.
     iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _  q
         with "WR [WRq]") as "[WR1 WR2]".
     { rewrite monPred_subjectively_unfold.
-      iDestruct (monPred_in_elim_vProp with "WRq") as (V') "?". by iExists V'. }
+      iDestruct (monPred_in_view_elim with "WRq") as (V') "?". by iExists V'. }
 
     set Q: time → unitProtocol → vProp :=
       (λ t'' s'',
@@ -1754,14 +1751,14 @@ Section arc.
         rewrite acq_sep_elim. iDestruct "Q" as "[SDA _]".
         iDestruct (acq_exist with "SDA") as (Dt) "SDA".
         iDestruct (acq_embed_elim with "SDA") as "SDA".
-        iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep.
-        iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep; iFrame "IS IW").
-        rewrite 2!bi.later_sep 2!monPred_in_sep. iSplitL "SMA"; last iSplitL "SDA";
+        iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep'.
+        iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep'; iFrame "IS IW").
+        rewrite 2!bi.later_sep 2!monPred_in_sep'. iSplitL "SMA"; last iSplitL "SDA";
           rewrite bi.later_exist; setoid_rewrite <- embed_later.
-        - rewrite -2!embed_exist monPred_in_embed. iDestruct "SMA" as (Mt) "SMA".
+        - rewrite -2!embed_exist monPred_in_embed'. iDestruct "SMA" as (Mt) "SMA".
           iExists Mt. by iFrame "SMA".
-        - rewrite -embed_exist monPred_in_embed. iExists _. iFrame "SDA".
-        - rewrite -2!embed_exist monPred_in_embed. iDestruct "WUA" as (Ut') "WUA".
+        - rewrite -embed_exist monPred_in_embed'. iExists _. iFrame "SDA".
+        - rewrite -2!embed_exist monPred_in_embed'. iDestruct "WUA" as (Ut') "WUA".
           iExists Ut'. by iFrame "WUA". }
       iModIntro. wp_case. wp_op. rewrite (bool_decide_false _ Eq).
       wp_case. by iApply ("HΦ"). }
@@ -1975,14 +1972,14 @@ Section arc.
         rewrite acq_sep_elim. iDestruct "Q" as "[SDA _]".
         iDestruct (acq_exist with "SDA") as (Dt') "SDA".
         iDestruct (acq_embed_elim with "SDA") as "SDA".
-        iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep.
-        iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep; iFrame "IS IW").
-        rewrite 2!bi.later_sep 2!monPred_in_sep. iSplitL "SMA"; last iSplitL "SDA";
+        iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep'.
+        iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep'; iFrame "IS IW").
+        rewrite 2!bi.later_sep 2!monPred_in_sep'. iSplitL "SMA"; last iSplitL "SDA";
           rewrite bi.later_exist; setoid_rewrite <- embed_later.
-        - rewrite -2!embed_exist monPred_in_embed. iDestruct "SMA" as (Mt') "SMA".
+        - rewrite -2!embed_exist monPred_in_embed'. iDestruct "SMA" as (Mt') "SMA".
           iExists Mt'. by iFrame "SMA".
-        - rewrite -embed_exist monPred_in_embed. iExists _. iFrame "SDA".
-        - rewrite -2!embed_exist monPred_in_embed. iDestruct "WUA" as (Ut') "WUA".
+        - rewrite -embed_exist monPred_in_embed'. iExists _. iFrame "SDA".
+        - rewrite -2!embed_exist monPred_in_embed'. iDestruct "WUA" as (Ut') "WUA".
           iExists Ut'. by iFrame "WUA". }
 
       iModIntro. wp_case. wp_op. rewrite (bool_decide_false _ Eq).
@@ -2200,14 +2197,14 @@ Section arc.
         rewrite acq_sep_elim. iDestruct "Q" as "[SMA _]".
         iDestruct (acq_exist with "SMA") as (Mt1) "SMA".
         iDestruct (acq_embed_elim with "SMA") as "SMA".
-        iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep.
-        iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep; iFrame "IS IW").
-        rewrite 2!bi.later_sep 2!monPred_in_sep. iSplitL "SMA"; last iSplitL "SDA";
+        iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep'.
+        iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep'; iFrame "IS IW").
+        rewrite 2!bi.later_sep 2!monPred_in_sep'. iSplitL "SMA"; last iSplitL "SDA";
           rewrite bi.later_exist; setoid_rewrite <- embed_later.
-        - rewrite -embed_exist monPred_in_embed. iExists Mt1. by iFrame "SMA".
-        - rewrite -2!embed_exist monPred_in_embed. iDestruct "SDA" as (?) "SDA".
+        - rewrite -embed_exist monPred_in_embed'. iExists Mt1. by iFrame "SMA".
+        - rewrite -2!embed_exist monPred_in_embed'. iDestruct "SDA" as (?) "SDA".
           iExists _. iFrame "SDA".
-        - rewrite -2!embed_exist monPred_in_embed. iDestruct "WUA" as (Ut') "WUA".
+        - rewrite -2!embed_exist monPred_in_embed'. iDestruct "WUA" as (Ut') "WUA".
           iExists Ut'. by iFrame "WUA". }
       iModIntro. wp_case. wp_op. rewrite (bool_decide_false _ Eq).
       wp_case. by iApply ("HΦ"). }
@@ -2548,7 +2545,7 @@ Section arc.
       iMod (GPS_SWWriter_dealloc (weak_interp P2 l γi γs γsw) _ _ true
              with "HINV IW WW") as "[wk _]"; [done|].
       wp_let. wp_op. wp_let. wp_op. wp_bind (_ <-ʳᵉˡ _)%E.
-      iApply (wp_write_rel _ #(1) with "[wk]");
+      iApply (wp_write _ #(1) with "[wk]");
         [done|by iApply own_loc_na_own_loc|..].
       iIntros "!> wk". wp_let. iApply "HΦ". by iFrame "str wk HP".