diff --git a/theories/finite.v b/theories/finite.v
index 9bde7e8770b4f730dc987b04f0ae523a464a4555..b2fa877ec8c197ec723e734a3823c8bb8e9d7b4c 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -382,7 +382,7 @@ Proof.
     - apply elem_of_list_fmap_1_alt with (x ↾ Hx); [apply elem_of_enum|]; done.
     - apply elem_of_list_fmap in Hx as [[x' Hx'] [-> _]]; done. }
   destruct (decide (x ∈ xs)); [left | right]; naive_solver.
-Qed.
+Qed. (* <- could be Defined but this lemma will probably not be used for computing *)
 
 Section sig_finite.
   Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.