diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index 37b32e3b9542c9fab394ae5039a3f60948ce206e..cdebeae48c1bd9185b6e0b8cb61fa9e8c2da6c92 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -253,6 +253,12 @@ Section cmra.
     - by rewrite left_id.
     - intros i. rewrite lookup_op lookup_empty. auto.
   Qed.
+  Lemma reservation_map_token_data_valid E k a :
+    k ∈ E → ✓ (reservation_map_token E ⋅ reservation_map_data k a) → False.
+  Proof.
+    rewrite reservation_map_valid_eq /= right_id_L left_id_L.
+    move=> ? [_] /(_ k). rewrite lookup_singleton. set_solver.
+  Qed.
 
   Lemma reservation_map_alloc E k a :
     k ∈ E → ✓ a → reservation_map_token E ~~> reservation_map_data k a.
diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 680d6c7ff5a02131456ba998f84e3a183fc52ea8..f06c87a93bebfc4ea60f4e7affadfff88f0ae104 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -260,6 +260,18 @@ Section gen_heap.
     rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
     exists 1%positive. by rewrite left_id_L.
   Qed.
+  Lemma meta_token_meta `{Countable A} E l (x : A) N :
+    ↑ N ⊆ E → meta_token l E -∗ meta l N x -∗ False.
+  Proof.
+    rewrite meta_token_unseal meta_unseal /meta_token_def /meta_def.
+    iIntros (?) "(%γm & Hγm & Hm) (%γm' & Hγm' & Hm')".
+    iCombine "Hγm Hγm'" gives %[_ <-].
+    iCombine "Hm Hm'" gives %[]%reservation_map_token_data_valid.
+    (* Same as what's proven above, at line 258; factor into lemma *)
+    cut (positives_flatten N ∈@{coPset} ↑N); first by set_solver.
+    rewrite namespaces.nclose_unseal. apply elem_coPset_suffixes.
+    exists 1%positive. by rewrite left_id_L.
+  Qed.
 
   (** Update lemmas *)
   Lemma gen_heap_alloc σ l v :