diff --git a/theories/finite.v b/theories/finite.v
index 9aac9ff0077feab5b2f99978eabf749cf9d63939..0cd64c40c3f9dea81fa091d4752503bfc2ce19bd 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -373,13 +373,6 @@ Qed.
 Lemma fin_card n : card (fin n) = n.
 Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
 
-Lemma finite_dec (P : Prop) `{Hfin : Finite P} : Decision P.
-Proof.
-  destruct Hfin as [[ | p proofs'] _ Hproofs].
-  { right. intros p. specialize (Hproofs p) as ?%not_elem_of_nil. naive_solver. }
-  { left. done. }
-Qed.
-
 (* shouldn’t be an instance (cycle with [sig_finite]): *)
 Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
   Decision (P x).