Forward compatibility for stdpp!555

theories/lifetime/model/primitive.v

@@ -36,7 +36,7 @@ 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.
-  iPureIntro. apply elem_of_dom. unfold to_ilftUR in *. simplify_map_eq.
+  iPureIntro. apply elem_of_dom. rewrite /to_ilftUR lookup_fmap in Hl.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.