diff --git a/iris_staging/algebra/max_prefix_list.v b/iris_staging/algebra/max_prefix_list.v
index ec1b0c2af1789deff3a2009fc745932565a01679..30f35f7c254a99cfcf29cd2cbbbdc7561290c877 100644
--- a/iris_staging/algebra/max_prefix_list.v
+++ b/iris_staging/algebra/max_prefix_list.v
@@ -39,12 +39,12 @@ Section max_prefix_list.
 
   Global Instance mono_list_lb_core_id (m : max_prefix_list A) : CoreId m := _.
 
-  Global Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
+  Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
   Proof.
     intros i. rewrite /to_max_prefix_list lookup_fmap.
     by destruct (map_seq 0 l !! i).
   Qed.
-  Global Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
+  Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
   Proof. apply cmra_valid_validN, to_max_prefix_list_valid. Qed.
 
   Local Lemma to_max_prefix_list_app l1 l2 :