diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 3f17636a0eaa98339be220a992f887f7375420f9..a54b3c8eb4c39e97de8acebb4ca1aa8e77508e69 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -97,9 +97,9 @@ Proof.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
         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.
-      iIntros (->).
-      exfalso. revert Hj1j2. rewrite /= singleton_op singleton_valid.
+    { iIntros (->). iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2.
+      exfalso; revert Hj1j2.
+      rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid.
       by intros [[]]. }
     iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
       as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 668036e24f219aebff67c22a76df28e2a685b121..ae9c563aad0173dde0ee0b44fbf5cf0b65462430 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -17,10 +17,10 @@ Proof.
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. by iFrame. }
   iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid.
-  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
-      (frac * agree bor_stateO)))) as (γbor) "[Hbor Hbor']";
-    first by apply auth_both_valid.
-  iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
+  iMod (own_alloc (● (∅ : gmap slice_name
+    (frac * agree bor_stateO)) ⋅ ◯ ∅)) as (γbor) "[Hbor Hbor']".
+  { by apply auth_both_valid. }
+  iMod (own_alloc (● (ε : gset_disj slice_name)))
      as (γinh) "Hinh"; first by apply auth_auth_valid.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".