diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7460dbef8eec073aab127068af6adc50e4035e29..54c7a4d41f50acce584e7a0cc38803311a62f9cd 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.2022-01-17.0.3e033cc4") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-01-17.1.eda41f52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index d8b6b66ea4922fb649d8e09acdac37146e1a22f8..2018feec9168994162f1087e50fae4244b7477ad 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -1523,7 +1523,7 @@ Section arc.
         rewrite decide_False; [done|by apply non_empty_singleton_L]. }
       iModIntro. iMod "Hclose1" as "_". iModIntro.
 
-      wp_case. iApply ("HΦ" with "[- $HP]"). iSplitL ""; [done|].
+      wp_case. iApply ("HΦ" with "[- $HP]").
       rewrite 2!monPred_objectively_elim. iFrame "HP1".
       iExists _,_,_, ∅. rewrite /StrongTok. iFrame "St'' tok'' R''".
       rewrite /StrMoves /StrDowns. iFrame "SM'' oW'' SD''".
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 39fd08d52265103ecbf3f3101633129f4bfc1ddb..a2d99b71338828575cddabbce0f3a43f08011329 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -28,7 +28,7 @@ Module Type lifetime_sig.
   (** * Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Local Declare Instance lft_intersect : Meet lft.
+  Global Declare Instance lft_intersect : Meet lft.
 
   Section defs.
   Notation monPred Σ Lat := (monPredI (lat_bi_index Lat) (uPredI (iResUR Σ))).
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 51ab71b8db4991ad70d4ca892e1d0439dfb777e8..63919e380202a473dcf2d245c1ea804a273d4338 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -138,14 +138,14 @@ Proof.
     destruct (decide (κ1 = κ)) as [->|], (decide (κ2 = κ)) as [->|];
       rewrite ?functions.fn_lookup_insert ?functions.fn_lookup_insert_ne //.
     + destruct (Hκmin κ2) as [_ []]=>//. apply strict_spec_alt. auto.
-    + rewrite -lat_join_sqsubseteq_r.
+    + rewrite <-lat_join_sqsubseteq_r.
       assert (Hκ1K : κ1 ∈ elements (filter (κ ⊂.) K)).
       { apply elem_of_elements. rewrite elem_of_filter.
         split; [|done]. apply strict_spec_alt. auto. }
       clear -Hκ1K. induction Hκ1K; solve_lat.
     + apply Hmono=>//; rewrite elem_of_difference elem_of_singleton; auto.
   - rewrite (big_sepS_delete _ K) //. iSplitL "Hinv".
-    + by rewrite functions.fn_lookup_insert -lat_join_sqsubseteq_l.
+    + rewrite functions.fn_lookup_insert. by rewrite <-lat_join_sqsubseteq_l.
     + iApply (@big_sepS_impl with "[$HK]"). iModIntro. iIntros (κ').
       rewrite elem_of_difference elem_of_singleton. iIntros ([??]) "H".
         rewrite functions.fn_lookup_insert_ne //.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 334b4e9611b6f7e7de54dfb3132109fd47863665..37b488cc520ed3baaca3569ec28257727b1c9de3 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -109,7 +109,7 @@ Proof.
   - iExists (<[γ:=bot]> B), (P ∗ Pinh)%I. rewrite !fmap_insert. iNext. by iFrame.
   - iExists γ. iSplitL.
     + iDestruct (monPred_in_intro True%I with "[//]") as (V) "[? _]".
-      iExists bot. iFrame. by rewrite [bot]lat_bottom_sqsubseteq.
+      iExists bot. iFrame. by rewrite <-lat_bottom_sqsubseteq.
     + iExists P. iIntros "{$Hslice} !> !> **". by iApply (bi.iff_refl True%I).
 Qed.