diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index ab9189f10029f3eda012b52257a0e6590a7fba1e..203e73dc685e6e294039ad6fdb7970ee9b359d97 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1727,7 +1727,7 @@ Section discrete_fun_cmra.
     by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
   Qed.
 
-  Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) :
+  Lemma discrete_fun_included_spec `{Finite A} (f g : discrete_fun B) :
     f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
     split; [by intros; apply discrete_fun_included_spec_1|].