diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index c9062f75e9480df3c6fb9f808d1f2e87b0e0d1cf..edec4c7609d3915651291f91eb547bec9202436c 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
-From lrust.typing Require Export uniq_bor shr_bor own sum.
+From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 4adb9c5134151815aea8edd47ec912a6462272bb..d261ffebbd96bf2fbf45cc91290a637a3c3c093d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -123,11 +123,11 @@ Section sum.
         by iApply (Hty2 with "* [] []"). }
     clear -Hleq. iSplit; last iSplit.
     - simpl. by rewrite Hleq.
-    - iNext. iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
+    - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
       iExists i, vl', vl''. iSplit; first done.
       iSplit; first by rewrite -Hleq.
       iDestruct ("Hty" $! i) as "(_ & #Htyi & _)". by iApply "Htyi".
-    - iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
+    - iAlways. iIntros (κ tid l) "H". iDestruct "H" as (i) "(Hmt & Hshr)".
       iExists i. iSplitR "Hshr".
       + rewrite /is_pad -Hleq. iDestruct ("Hty" $! i) as "(Hlen & _)".
         iDestruct "Hlen" as %<-. done.