diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7ab5190e0edd564f30121a06c7b04b465402b5be..c8e90773c245b008c6f5c39d7b2af5fa1247c75f 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-07-22.0.26ebf1ee") | (= "dev") }
+  "coq-iris" { (= "dev.2021-07-23.2.572da574") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index fadb50891124401a97a57493a95952f8f020d5fe..4cd8f7ca47b496d09971d991b966b0df6eb5edf5 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -95,11 +95,7 @@ Section rwlockreadguard_functions.
           rewrite -EQ. iDestruct "EQν" as %<-%(inj to_agree)%leibniz_equiv.
           iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
           iApply (step_fupd_mask_mono ((↑lftN ∪ lft_userE) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE)));
-            last iApply (step_fupd_mask_frame_r _ (lft_userE)).
-          { solve_ndisj. }
-          { solve_ndisj. }
-          { rewrite difference_difference. apply: disjoint_difference_r1. done. }
-          { solve_ndisj. }
+            last iApply (step_fupd_mask_frame_r _ (lft_userE)); [solve_ndisj..|].
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
           iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
           { set_solver+. }