diff --git a/opam.pins b/opam.pins
index ad8c09a8a7d1f15d589d3ab884d5053aa6d86498..202664902296013ad5d1896abfca2d49917d8de5 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq a1bf05fe892801c43a9d61e8cb7cf7cb1f1eced3
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 1e241cca15302ae89d41f14251c2dafbd7efebb6
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b0cb325a52a32f269254370fd1dfb214c10c67b8..976381bbc9511de555c3678a6fca1e07b6f21db6 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -88,7 +88,7 @@ Section rc.
         iExists _, _, _. iFrame. done. }
       iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & Htok & #Hshr)".
       iMod ("Hclose2" with "[] [Hrc Htok]") as "[HX Htok]".
-      { iNext. iIntros "HX". iModIntro. (* FIXME: iNext here doesn't strip of the next from in front of the evar. *)
+      { iNext. iIntros "HX". iModIntro. iNext.
         iRight. iExists γ, ν, q'. iExact "HX". }
       { iNext. by iFrame "#∗". }
       iAssert (|={F ∖ ↑shrN}=> C)%I with "[HX]" as ">#HC".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 3fadde0b8ca447a3f30833177927a510ff8edc57..5ef44d371e164eb3ffe28dcb59eda9b05c5408ca 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -205,11 +205,10 @@ Section sum.
       { rewrite <-HF. simpl. rewrite <-union_subseteq_r.
         apply shr_locsE_subseteq. omega. }
       iDestruct (na_own_acc with "Htl") as "[$ Htlclose]".
-      { (* Really, we don't even have a lemma for anti-monotonicity of difference...? *)
-        cut (shr_locsE (shift_loc l 1) (ty_size (nth i tyl ∅)) ⊆
-                  shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
-        - simpl. set_solver+.
-        - apply shr_locsE_subseteq. omega. }
+      { apply difference_mono_l.
+        trans (shr_locsE (shift_loc l 1) (list_max (map ty_size tyl))).
+        - apply shr_locsE_subseteq. omega.
+        - set_solver+. }
       destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
       rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; apply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).