diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 3405d59a847828305cbe4bc60f0c316031a2ef5f..c3c4f2acb1f6d232c1b02ab85723a88747d9e234 100644
--- a/lifetime/model/primitive.v
+++ b/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.