diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index d41aaba88737f596ab21c2e81c839b7dbaa03753..d2774d16c479c21cec1392d80cf9797b0cb50e82 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -129,7 +129,7 @@ Section gset_bij.
     by iApply gset_bij_own_elem_get_big.
   Qed.
   Lemma gset_bij_own_alloc_empty :
-    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 ∅.
+    ⊢ |==> ∃ γ, gset_bij_own_auth γ 1 (∅ : gset (A * B)).
   Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
 
   Lemma gset_bij_own_extend {γ L} a b :