Forward compatibility fix for iris/stdpp!555

lifetime/model/primitive.v

@@ -38,7 +38,8 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
     as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
-  unfold to_ilftUR in *. simplify_map_eq.
+  revert Hl. rewrite /to_ilftUR lookup_fmap.
+  case: (I !! _)=> [γs'|] Hl; first by eauto.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.