use solve_ndisj more

theories/lifetime/model/creation.v

@@ -180,10 +180,7 @@ Proof.
     iDestruct (monPred_in_intro True%I with "[//]") as (V) "[H _]".
     by rewrite -(lat_bottom_sqsubseteq V). }
   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".
   iMod (ilft_create _ _ {[+ Λ +]} with "HA HI Hinv") as "H". clear A I.
   iDestruct "H" as (A I) "(% & HA & HI & Hinv)".
@@ -222,15 +219,7 @@ Proof.
       + edestruct HK=>//. set_solver + Hal HΛκ HκK HI.
     - move=>-[[[[??]?]|?][?|?]]//. by destruct (lft_alive_and_dead_in A κ). }
   rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[HinvD HinvK]".
-  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_trans. iApply (fupd_mask_mono (userE ∪ ↑borN ∪ ↑inhN)); first solve_ndisj.
   iMod (lfts_kill A I K K' Vs with "[$HI HinvD] [HinvK]") as "[[HI HinvD] HinvK]"=>//.
   { intros κ κ' Hκ Hκ' Hκκ'. assert (κ ∈ dom (gset _) I) by set_solver +HI Hκ. auto. }
   { move=> κ κ'. rewrite !elem_of_K=>-[?[Hd|?]] ??; split=>//.