bump Iris; use solve_ndisj more

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}%"]

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+. }