diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 56a094f1eacf5e2ed474b62fe7797fac53e090e7..286ea584cc95f7c21832b6fcea3cdb71398ee660 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.15.1:
+build-coq.8.17.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1"
+    OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
   tags:
   - fp-timing
diff --git a/README.md b/README.md
index 885b5a68c3d25192dee94c2380ef98fab3a212f4..0f7408537c71f201c4f7ebb51ea1b966c40919f2 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is the Coq development accompanying RBrlx.
 
 This version is known to compile with:
 
- - Coq 8.15.1
+ - Coq 8.17.0
  - A development version of [GPFSL].
 
 ## Building from source
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 8439145be284fbed0e8589e6acbf0d2af64f811c..748c8e270a583ec7e4dda4aba58b68dc5fa02762 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.2023-03-23.0.20ac1d8c") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-05-02.2.34a8bf9d") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index f30bbf1cf49a0ac1e6c0bee1f0fcf40b18714b0c..c2f5d1d4b3a55422e5309272d8b1dcb8d01453ff 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -597,14 +597,17 @@ Section arc.
                        ⎡ own γ ((ε, ◯ ((Some 1%Qp, ε)), ε) : arcUR) ⎤)%I as ">Own".
     { do 9 setoid_rewrite <- embed_sep. do 9 setoid_rewrite <- own_op.
       iMod (own_alloc (A:=arcUR)) as (γ) "Own"; last by iExists γ.
-      rewrite -5!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
-                          (prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
-      rewrite /= -2!pair_op /= !left_id /=. split.
-      { by split; apply auth_both_valid_discrete. }
-      do 2 setoid_rewrite <-pair_op. rewrite /= !left_id !right_id.
-      split; split; [..|by apply auth_both_valid_discrete|by apply auth_auth_valid];
-        (split; [by apply auth_both_valid_discrete|rewrite /= right_id]);
-        [|rewrite left_id]; by apply auth_auth_valid. }
+      split; split; simpl.
+      - rewrite !right_id. by apply auth_both_valid_discrete.
+      - rewrite !left_id. by apply auth_both_valid_discrete.
+      - split; split; simpl; rewrite !left_id !right_id.
+        + by apply auth_both_valid_discrete.
+        + by apply auth_auth_valid.
+        + by apply auth_both_valid_discrete.
+        + by apply auth_auth_valid.
+      - split; simpl; rewrite !left_id !right_id.
+        + by apply auth_both_valid_discrete.
+        + by apply auth_auth_valid. }
     iDestruct "Own" as (γsw)
       "(SA & St & WA & SMA & [SM1 SM2] & SDA & [SD1 SD2] & WUA & WU & [S1 S2])".
     iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
@@ -654,14 +657,17 @@ Section arc.
                        WeakUpAuth γ ∅ ∗ WkUps γ 1%Qp ∅)%I as ">Own".
     { do 8 setoid_rewrite <- embed_sep. do 8 setoid_rewrite <- own_op.
       iMod (own_alloc (A:=arcUR)) as (γ) "?"; last by iExists γ.
-      rewrite -4!(@pair_op (prodUR (authUR strong_stUR) (authUR weak_stUR))
-                          (prodUR (prodUR move_selfUR move_otherUR) move_otherUR)).
-      rewrite /= -2!pair_op /= !left_id /=. split.
-      { by split; apply auth_both_valid_discrete. }
-      do 2 setoid_rewrite <-pair_op. rewrite /= !left_id !right_id.
-      split; split; [..|by apply auth_both_valid_discrete|by apply auth_auth_valid];
-        (split; [by apply auth_both_valid_discrete|rewrite /= right_id]);
-        [|rewrite left_id]; by apply auth_auth_valid. }
+      split; split; simpl.
+      - rewrite !right_id. by apply auth_auth_valid.
+      - rewrite !left_id !right_id. by apply auth_both_valid_discrete.
+      - split; split; simpl; rewrite !left_id !right_id.
+        + by apply auth_both_valid_discrete.
+        + by apply auth_auth_valid.
+        + by apply auth_both_valid_discrete.
+        + by apply auth_auth_valid.
+      - split; simpl; rewrite !left_id ?right_id.
+        + by apply auth_both_valid_discrete.
+        + by apply auth_auth_valid. }
     iDestruct "Own" as (γsw) "(SA & WA & Wt & SMA & SM & SDA & SD & WUA & [WU1 WU2])".
     iMod (view_inv_alloc_frac N _ (1/2 + 1/2/2) (1/2/2)) as (γi) "[[tok2 tok1] VI]";
       first by rewrite -Qp.add_assoc 2!Qp.div_2.
@@ -982,10 +988,8 @@ Section arc.
         with "[St] tok [SR]  [SM] [] [SD] [] oW") as "HP";
         [by iExact "St"|by iExists _|..|by rewrite right_id_L|done|].
       { rewrite /Mt'. case decide => _; [done|by rewrite right_id_L]. }
-      { case (decide (Z.to_pos _ = _)) => ?; [|done].
-        rewrite decide_False; [|by apply non_empty_singleton_L].
+      { destruct (decide (Z.to_pos _ = _)); [|done].
         iExists _,_. iFrame "RR'". iPureIntro. move => ? /elem_of_singleton -> //. }
-
       iModIntro. iMod "Hclose1" as "_". iModIntro.
       wp_case. iApply ("HΦ" with "[- $HP]"). iFrame "HP1".
       iExists _,_,∅. rewrite /StrongTok. iFrame "St'' tok'' R''".
@@ -1178,8 +1182,7 @@ Section arc.
 
       iMod ("Hclose2" $! ∅ Dt' with "St tok SR [SM] [] SD [] oW") as "HP";
         [by rewrite right_id_L|done|..].
-      { rewrite /Dt'. case decide; [|done].
-        rewrite decide_False; [done|by apply non_empty_singleton_L]. }
+      { rewrite /Dt'. by case_decide. }
       iModIntro. iMod "Hclose1" as "_". iModIntro.
       wp_case. iApply ("HΦ" with "[- $HP]").
       iExists _, ∅. iFrame "Wt' WRs".
@@ -1519,8 +1522,7 @@ Section arc.
       { iApply (arc_inv_join with "SMA SDA [WUA] IS IW"). by iExists _. }
       iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
       iMod ("Hclose2" with "Wt tok WRq [WU] []") as "HP"; [by iExact "WU"|..].
-      { rewrite /Ut'. case decide; [|done].
-        rewrite decide_False; [done|by apply non_empty_singleton_L]. }
+      { rewrite /Ut'. by case_decide. }
       iModIntro. iMod "Hclose1" as "_". iModIntro.
 
       wp_case. iApply ("HΦ" with "[- $HP]").
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 866f5e88db292f673ef7495277701c4dc5704d8f..fbcaeea7a3f1caa104d8b0e51f1efdeab45c2bae 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -239,10 +239,10 @@ Section ArcGhost.
   Proof.
     rewrite -3!embed_sep -3!own_op. iIntros "own".
     iMod (own_update with "own") as "$"; [|done].
-    apply prod_update; [done|].
-    apply prod_update; [|rewrite /= left_id right_id //].
+    apply prod_update; simpl; [done|].
+    apply prod_update; simpl; [|done].
     setoid_rewrite <-pair_op. rewrite /=.
-    apply prod_update; [|rewrite /= left_id right_id //].
+    apply prod_update; simpl; [|done].
     rewrite /= -2!pair_op /= 2!right_id left_id.
     apply prod_update; simpl.
     - by apply auth_update, option_local_update, exclusive_local_update.
@@ -339,10 +339,10 @@ Section ArcGhost.
   Proof.
     rewrite -3!embed_sep -3!own_op. iIntros "own".
     iMod (own_update with "own") as "$"; [|done].
-    apply prod_update; [done|]. simpl.
-    apply prod_update; [|rewrite /= !right_id //].
+    apply prod_update; simpl; [done|].
+    apply prod_update; simpl; [|done].
     setoid_rewrite <-pair_op. rewrite /=.
-    apply prod_update; [rewrite /= !right_id //|].
+    apply prod_update; simpl; [done|].
     rewrite /= -2!pair_op /= 2!right_id left_id. rewrite -2!lat_op_join'.
     apply prod_update; simpl.
     - apply auth_update, option_local_update, prod_local_update_2.
@@ -358,7 +358,7 @@ Section ArcGhost.
     (WkUps γ q Ut ∗ WkUps γ q' Ut')%I.
   Proof.
     rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
-    by do 3 (apply pair_proper; [done|]).
+    by do 3 (apply pair_proper; simpl; [done|]).
   Qed.
 
   Lemma WkUps_full_exclusive γ q Ut' :
@@ -380,8 +380,8 @@ Section ArcGhost.
   Proof.
     rewrite -3!embed_sep -3!own_op. iIntros "own".
     iMod (own_update with "own") as "$"; [|done].
-    apply prod_update; [done|]. simpl.
-    apply prod_update; [rewrite /= !right_id //|].
+    apply prod_update; simpl; [done|].
+    apply prod_update; simpl; [done|].
     apply prod_update; rewrite /=.
     - apply auth_update, option_local_update, prod_local_update_2.
       rewrite -2!lat_op_join' (cmra_comm_L (to_latT Ut1)) (cmra_comm_L (to_latT Ut2)).
@@ -437,7 +437,7 @@ Section ArcGhost.
   Proof.
     iIntros "own". rewrite -embed_sep -own_op.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; simpl; [|by rewrite right_id].
+    apply prod_update; simpl; [|done].
     apply prod_update; simpl; [|done]. apply auth_update_alloc.
     rewrite /= -(right_id None op (Some _)). by apply: op_local_update_discrete.
   Qed.
@@ -449,7 +449,7 @@ Section ArcGhost.
   Proof.
     iIntros "own". rewrite -embed_sep -own_op.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; simpl; [|by rewrite right_id].
+    apply prod_update; simpl; [|done].
     apply prod_update; simpl; [|done]. apply auth_update_alloc.
     rewrite Pos.add_comm Qp.add_comm -pos_op_add /= -frac_op pair_op Some_op.
     rewrite -{2}(right_id None op (Some ((q' /2)%Qp, _))).
@@ -464,7 +464,7 @@ Section ArcGhost.
   Proof.
     iIntros "own". rewrite -embed_sep -own_op.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; simpl; [|by rewrite right_id].
+    apply prod_update; simpl; [|done].
     apply prod_update; simpl; [done|]. apply auth_update_alloc.
     apply prod_local_update; simpl; [done|].
     rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
@@ -506,7 +506,8 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [|done].
+    apply prod_update; [|simpl; by rewrite right_id].
+    apply prod_update; simpl; [|done].
     apply auth_update_dealloc.
     rewrite -frac_op -pos_op_add /= (cmra_comm_L q) pair_op Some_op.
     by apply (cancel_local_update_unit (Some _)), _.
@@ -518,7 +519,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
+    apply prod_update; [|by rewrite /= right_id]. apply prod_update; simpl; [done|].
     apply auth_update_dealloc. apply prod_local_update; [done|].
     rewrite /= -(right_id None op (Some _)). apply: cancel_local_update_unit.
   Qed.
@@ -530,7 +531,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [done|].
+    apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; simpl; [done|].
     apply auth_update_dealloc. apply prod_local_update; [done|].
     rewrite -frac_op -pos_op_add /= (cmra_comm_L q) pair_op Cinl_op Some_op.
     by apply (cancel_local_update_unit (Some _)), _.
@@ -560,7 +561,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
+    apply prod_update; [|by rewrite /= right_id]. apply prod_update; simpl; [done|].
     apply auth_update_dealloc. apply prod_local_update; [|done].
     rewrite /= -{1}(right_id None op (Some _)).
     by apply (cancel_local_update_unit (Some _)), _.
@@ -597,7 +598,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|]. simpl.
+    apply prod_update; [|by rewrite /= right_id]. apply prod_update; simpl; [done|].
     apply auth_update_alloc. apply prod_local_update; simpl; [done|].
     rewrite -(right_id None op (Some _)).
     by apply op_local_update_discrete.
@@ -627,7 +628,7 @@ Section ArcGhost.
     iIntros "own". iDestruct (WeakAuth_lock_agree with "own") as %Eq.
     rewrite -embed_sep -own_op.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
-    apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|]. simpl.
+    apply prod_update; [|by rewrite /= right_id]. apply prod_update; simpl; [done|].
     rewrite Eq. apply auth_update_dealloc. apply prod_local_update; [done|].
     rewrite /= -{1}(right_id None op (Some _)).
     apply (cancel_local_update_unit (Some _)), _.