diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 297e55c80d04fb226ac4a8cc70136e54c309c0ad..79112c3fa39170854b808dce42c4a1716a7219fd 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -32,7 +32,7 @@ Section mono_proof.
   Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
   Proof. apply _. Qed.
 
-  Lemma newcounter_mono_spec (R : iProp Σ) :
+  Lemma newcounter_mono_spec :
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".