diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 29cff8106c3d0b3ee8fdd31a44f4042ca68d3b94..7ab5190e0edd564f30121a06c7b04b465402b5be 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-19.2.0ae9d9ee") | (= "dev") }
+  "coq-iris" { (= "dev.2021-07-22.0.26ebf1ee") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index dbfdff98dff95b716b776af3e371a2e29d9caa15..e9dd05da2363a31baffc7a6344ad98b2f539f993 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -33,8 +33,7 @@ Proof.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_both_valid_discrete; lia. }
-  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
-  { (* FIXME [solve_ndisj] fails *) set_solver+. }
+  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first by solve_ndisj.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
   iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
@@ -131,13 +130,8 @@ Proof.
   iModIntro; iExists Λ.
   rewrite {1}/lft_tok big_sepMS_singleton. iSplit; first done. iFrame "HΛ".
   clear I A HΛ. iIntros "!> HΛ".
-  iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)).
-  { (* FIXME solve_ndisj should really handle this... *)
-    assert (↑mgmtN ## userE) by solve_ndisj. set_solver. }
-  { done. }
+  iApply (step_fupd_mask_mono (↑lftN ∪ userE) _ ((↑lftN ∪ userE)∖↑mgmtN)); [solve_ndisj..|].
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  { (* FIXME solve_ndisj should really handle this... *)
-    assert (↑mgmtN ⊆ ↑lftN) by solve_ndisj. set_solver. }
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
     as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid_discrete.
@@ -159,15 +153,7 @@ Proof.
   { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!>".
     iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
   iApply fupd_trans.
-  iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)).
-  { (* FIXME can we make solve_ndisj handle this? *)
-    clear -userE_lftN_disj. rewrite -assoc. apply union_least.
-    - assert (userE ##@{coPset} ↑mgmtN) by solve_ndisj. set_solver.
-    - assert (↑inhN ##@{coPset} ↑mgmtN) by solve_ndisj.
-      assert (↑inhN ⊆@{coPset} ↑lftN) by solve_ndisj.
-      assert (↑borN ##@{coPset} ↑mgmtN) by solve_ndisj.
-      assert (↑borN ⊆@{coPset} ↑lftN) by solve_ndisj.
-      set_solver. }
+  iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)); first solve_ndisj.
   iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
   { done. }
   { intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 7eed83f49bdfdbf9b2c1ef151525bb56f2464da8..0cf17a54ecf73839606c40a4a629e6237610e207 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -770,8 +770,7 @@ Section arc.
       rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦1]".
       iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
       iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
-      { set_solver+. (* FIXME [solve_ndisj] fails *) }
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
       iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
       wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
@@ -874,8 +873,7 @@ Section arc.
       rewrite heap_mapsto_vec_cons. iDestruct "Hr" as "[Hr0 Hr1]".
       iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
       iSpecialize ("H†" with "Hν").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver+. }
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
       wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
       rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
       iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
@@ -949,8 +947,7 @@ Section arc.
     iDestruct "Hrc" as (γ ν q') "[#(Hi & Hs & #Hc) Htoks]".
     wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
     - iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver+. }
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
       wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
       iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
       { iIntros "!> Hown !>". iLeft. iFrame. }
@@ -1035,8 +1032,7 @@ Section arc.
     pose proof (fin_to_nat_lt x). destruct (fin_to_nat x) as [|[|[]]]; last lia.
     - iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
       iSpecialize ("Hc" with "HP1").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver+. }
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
       wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
       iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
       { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -1051,8 +1047,7 @@ Section arc.
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
     - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _). 
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver+. }
+      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); [solve_ndisj..|].
       wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
       rewrite -!lock Nat2Z.id.
       wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index e2c0553d8920c817ac8a5b3ef5566796a9677e32..fadb50891124401a97a57493a95952f8f020d5fe 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -96,11 +96,10 @@ Section rwlockreadguard_functions.
           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)).
-          { set_solver+. }
+          { solve_ndisj. }
           { solve_ndisj. }
           { rewrite difference_difference. apply: disjoint_difference_r1. done. }
-          { (* FIXME [solve_ndisj] fails. *)
-            apply: disjoint_difference_r1. done. }
+          { 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+. }