diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7334ae546cdc2e7308431a1e0d8da2bba10040e0..73255a411bffab5cbc150482251201c8764ed16d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,6 +73,7 @@ lemma.
   and `saved_pred_own`, so they can be updated. The previous persistent versions
   can be recovered with the fraction `DfracDiscarded`. Allocation lemmas now take
   a `dq` parameter to define the initial fraction.
+* Remove an unused fraction argument to `dfrac_valid_discarded`.
 
 **Changes in `program_logic`:**
 
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 30969cbbaffb53703eeb818f854bd1c07a9e3659..3511d31b66bfeb7faedd0c87eb28329c80fa3cb4 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -173,7 +173,7 @@ Section dfrac.
   Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
   Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
 
-  Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
+  Lemma dfrac_valid_discarded : ✓ DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_valid_own_discarded q :