diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 430fec3d41676dd352d221eb3af67e87db3bef5e..8d19bd9e345c03b2663c60c8f200d1bd65057508 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -155,7 +155,7 @@ Section contrib_spec.
 
   Lemma read_contrib_spec_1 γ l n :
     {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l
-    {{{ n, RET #n; ccounter γ 1 n }}}.
+    {{{ RET #n; ccounter γ 1 n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.