Forwards compatibility fixes with iris!516.

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.

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]".