diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 4c03ecd64d4b83788118dd2828bf1e515403e842..f8a5aea4c83b6f3d838455f118c9f3e623c2be6f 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -610,7 +610,7 @@ Global Instance bupd_proper : Proper ((≡) ==> (≡)) (@uPred_bupd M) := ne_pro
 
 (** PlainlyExist1BI *)
 
-Lemma uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
+Global Instance uPred_plainly_exist_1 : PlainlyExist1BI (uPredI M).
 Proof. unfold PlainlyExist1BI. by unseal. Qed.
 
 (** Limits *)