diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 74302c169ba8b9da0da2822f9a72890e5359db27..ecbbd0604faa3cfc90d6f624bdf2eefdebf7800b 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2022-11-30.1.e52255ba") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/coq-orc11.opam b/coq-orc11.opam
index 4073fa0a0db587c0ba9b37e02d3b6e7e018d9fa1..282de8d1d87ccd528b34dab6aae3545de0b5a70b 100644
--- a/coq-orc11.opam
+++ b/coq-orc11.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
 
 depends: [
-  "coq-stdpp" { (= "dev.2022-11-30.0.ffa862a8") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-02-04.0.7125e166") | (= "dev") }
 ]
 
 build: ["./make-package" "orc11" "-j%{jobs}%"]
diff --git a/gpfsl-examples/lock/proof_ticket_lock_gps.v b/gpfsl-examples/lock/proof_ticket_lock_gps.v
index a7e76fcaa58e10e74918f19d1068940c3138fda5..44bd1a55dfcfd9531e32f82617b5db2d001b2dc5 100644
--- a/gpfsl-examples/lock/proof_ticket_lock_gps.v
+++ b/gpfsl-examples/lock/proof_ticket_lock_gps.v
@@ -46,7 +46,7 @@ Definition Waiting M n : gset nat :=
   filter (λ i, ∃ t, M !! i = Excl2 t ∧ n ≤ t) (dom M).
 Definition Ws M n : nat := size (Waiting M n).
 
-Definition ns_tkt_bound M t n : Prop := 
+Definition ns_tkt_bound M t n : Prop :=
   n ≤ t ∧ t ≤ n + Ws M n
   ∧ ∀ (i k: nat), M !! i = Excl2 k →
       (k < t) ∧ ∀ (j: nat), M !! j = Excl2 k → i = j.
@@ -254,7 +254,7 @@ Proof.
       split; [|split; first lia; split].
       * eapply Z.le_lt_trans; first by apply LE2.
         apply Z.add_lt_le_mono; [lia|]. by apply Waiting_size_le.
-      * rewrite Nat2Z.inj_succ Nat2Z.inj_add Zplus_assoc_reverse 
+      * rewrite Nat2Z.inj_succ Nat2Z.inj_add Zplus_assoc_reverse
                 (Z.add_comm 1) Zplus_assoc.
         apply Zplus_le_compat_r. etrans; first apply LE2.
         assert (Eqs :=
@@ -283,7 +283,7 @@ Proof.
           { rewrite disjoint_singleton_l /Waiting elem_of_filter.
             rewrite Ini. move => [[? [[<-] ?]] _]. lia. }
           rewrite Nat2Z.inj_add size_singleton Nat2Z.inj_add
-                  (Z.add_comm 1) Zplus_assoc. 
+                  (Z.add_comm 1) Zplus_assoc.
           by apply Zplus_le_compat_r. }
       * by apply ns_inj_insert.
   - exists n. split; [done|split]; first by right.
@@ -300,7 +300,7 @@ Proof.
         { rewrite disjoint_singleton_l /Waiting elem_of_filter.
           rewrite Ini. move => [[? [//]]]. }
         rewrite Nat2Z.inj_add size_singleton Nat2Z.inj_add
-                (Z.add_comm 1) Zplus_assoc. 
+                (Z.add_comm 1) Zplus_assoc.
         by apply Zplus_le_compat_r. }
     * by apply ns_inj_insert.
 Qed.
@@ -370,7 +370,7 @@ Proof.
   apply bi.sep_ne; [done|].
   repeat (apply bi.exist_ne => ?).
   apply GPS_iSP_Writer_contractive; [done|].
-  destruct n; [done|by simpl].
+  dist_later_fin_intro. eapply H; si_solver.
 Qed.
 
 Definition NSP P γ : interpO Σ natProtocol := fixpoint (NSP' P γ).
diff --git a/gpfsl-examples/queue/proof_ms_gps.v b/gpfsl-examples/queue/proof_ms_gps.v
index cc332bd15d3b8563127dfc76d3f87dd45b946732..f885eb5a03def42e8d200c13df027ab25b79573a 100644
--- a/gpfsl-examples/queue/proof_ms_gps.v
+++ b/gpfsl-examples/queue/proof_ms_gps.v
@@ -82,8 +82,8 @@ Proof.
   do 2 apply bi.exist_ne => ?.
   apply bi.sep_ne; [done|].
   do 2 (apply bi.exist_ne => ?).
-  apply GPS_iPP_contractive. destruct n => //.
-  by apply H.
+  apply GPS_iPP_contractive.
+  dist_later_fin_intro. eapply H; si_solver.
 Qed.
 
 Definition Link : ∀ γ, interpO Σ LinkProtocol := fixpoint Link'.
diff --git a/gpfsl/gps/surface_iPP.v b/gpfsl/gps/surface_iPP.v
index e25f9156af9149df2f8c6c77e1e374a05f796f81..c225d538072bba8d5601b273e86ec43efb5cc21d 100644
--- a/gpfsl/gps/surface_iPP.v
+++ b/gpfsl/gps/surface_iPP.v
@@ -274,7 +274,7 @@ Global Instance GPS_iPP_contractive l t s v γ :
   Contractive (λ IP, GPS_iPP IP l t s v γ).
 Proof.
   move => n ???. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
-  destruct n; [done|]. by apply GPS_PPInv_ne.
+  dist_later_fin_intro. apply GPS_PPInv_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_iPP_ne l t s v γ :
   NonExpansive (λ IP, GPS_iPP IP l t s v γ).
diff --git a/gpfsl/gps/surface_iSP.v b/gpfsl/gps/surface_iSP.v
index c3602849b95f2d7f94606c0b188d0f184caf5b3a..016b2089cfeae6b6b369e6adef14940c65f67562 100644
--- a/gpfsl/gps/surface_iSP.v
+++ b/gpfsl/gps/surface_iSP.v
@@ -328,7 +328,7 @@ Global Instance GPS_iSP_Writer_contractive n l t s v γ :
          (λ IP IPC, GPS_iSP_Writer IP IPC l t s v γ).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_iSP_Writer_ne l t s v γ :
   NonExpansive2 (λ IP IPC, GPS_iSP_Writer IP IPC l t s v γ).
@@ -348,7 +348,7 @@ Global Instance GPS_iSP_Reader_contractive n l t s v γ :
          (λ IP IPC, GPS_iSP_Reader IP IPC l t s v γ).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_iSP_Reader_ne l t s v γ :
   NonExpansive2 (λ IP IPC, GPS_iSP_Reader IP IPC l t s v γ).
@@ -368,7 +368,7 @@ Global Instance GPS_iSP_SharedReader_contractive n l t s v q γ :
          (λ IP IPC, GPS_iSP_SharedReader IP IPC l t s v q γ).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_iSP_SharedReader_ne l t s v q γ :
   NonExpansive2 (λ IP IPC, GPS_iSP_SharedReader IP IPC l t s v q γ).
@@ -388,7 +388,7 @@ Global Instance GPS_iSP_SharedWriter_contractive n l t s v γ :
          (λ IP IPC, GPS_iSP_SharedWriter IP IPC l t s v γ).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply subj_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_iSP_SharedWriter_ne l t s v γ :
   NonExpansive2 (λ IP IPC, GPS_iSP_SharedWriter IP IPC l t s v γ).
diff --git a/gpfsl/gps/surface_vSP.v b/gpfsl/gps/surface_vSP.v
index 220176fcd18cad8ad812d2fa6668a75a38018536..6f41cc4513be3f8b2defa33b9338f16eb7e746f9 100644
--- a/gpfsl/gps/surface_vSP.v
+++ b/gpfsl/gps/surface_vSP.v
@@ -148,7 +148,7 @@ Global Instance GPS_vSP_Writer_contractive n l t s v γ γi :
          (λ IP IPC, GPS_vSP_Writer IP IPC l t s v γ γi).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_vSP_Writer_ne IPC l t s v γ γi :
   NonExpansive2 (λ IP IPC, GPS_vSP_Writer IP IPC l t s v γ γi).
@@ -168,7 +168,7 @@ Global Instance GPS_vSP_Reader_contractive n l t s v γ γi :
          (λ IP IPC, GPS_vSP_Reader IP IPC l t s v γ γi).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_vSP_Reader_ne l t s v γ γi :
   NonExpansive2 (λ IP IPC, GPS_vSP_Reader IP IPC l t s v γ γi).
@@ -188,7 +188,7 @@ Global Instance GPS_vSP_SharedReader_contractive n l t s v q γ γi :
          (λ IP IPC, GPS_vSP_SharedReader IP IPC l t s v q γ γi).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_vSP_SharedReader_ne l t s v q γ γi :
   NonExpansive2 (λ IP IPC, GPS_vSP_SharedReader IP IPC l t s v q γ γi).
@@ -208,7 +208,7 @@ Global Instance GPS_vSP_SharedWriter_contractive n l t s v γ γi :
          (λ IP IPC, GPS_vSP_SharedWriter IP IPC l t s v γ γi).
 Proof.
   move => ??????. apply bi.sep_ne; [done|]. apply view_inv_contractive.
-  destruct n; [done|]. by apply GPS_INV_ne.
+  dist_later_fin_intro. apply GPS_INV_ne; by eapply dist_later_S.
 Qed.
 Global Instance GPS_vSP_SharedWriter_ne l t s v γ γi :
   NonExpansive2 (λ IP IPC, GPS_vSP_SharedWriter IP IPC l t s v γ γi).