diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8801035c6188ceb4af22d8998aac7f8331f2f58d..5a6020add4d65ae0f07383c8efd5ffb1625fd354 100644
--- a/theories/lifetime/model/primitive.v
+++ b/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.