diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 663e7c018ea37c7dc0ccea8a93a0875c50fef6cd..61471b2ba8cb67ff73c113538194303d7e6fb10c 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -98,7 +98,7 @@ Proof.
as %[EQB2%to_borUR_included _]%auth_both_valid.
iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
{ iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
- iPureIntro. iIntros (->). (* FIXME this used to work without iPureIntro. *)
+ iIntros (->).
exfalso. revert Hj1j2. rewrite /= singleton_op singleton_valid.
by intros [[]]. }
iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index da1434ef355a5cbb61e78e3ec50be01a37163921..146ec89210ea98d8d80e1600a703667fe20a03e0 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -184,13 +184,13 @@ Section borrow.
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']"; first solve_ndisj.
iApply (wp_step_fupd _ _ (_∖_) with "[Hown Htok2]"); try done.
- - iApply ("Hown" with "[%] Htok2"); first solve_ndisj.
- - iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
- iMod ("Hclose''" with "Htok2") as "Htok2".
- iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
- iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
- rewrite tctx_interp_singleton tctx_hasty_val' //.
- by iApply (ty_shr_mono with "Hincl' Hshr").
+ { iApply ("Hown" with "[%] Htok2"); first solve_ndisj. }
+ iApply wp_fupd. wp_read. iIntros "!>[#Hshr Htok2]".
+ iMod ("Hclose''" with "Htok2") as "Htok2".
+ iMod ("Hclose'" with "[H↦]") as "Htok1"; first by auto.
+ iMod ("Hclose" with "[Htok1 Htok2]") as "($ & $)"; first by iFrame.
+ rewrite tctx_interp_singleton tctx_hasty_val' //.
+ by iApply (ty_shr_mono with "Hincl' Hshr").
Qed.
Lemma type_deref_shr_uniq {E L} κ κ' x p e ty C T T' :