From 79830523c8f4500a96664ca23c5403ae2c2feb65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Glen=20M=C3=A9vel?= <glen.mevel@inria.fr>
Date: Mon, 13 Dec 2021 17:32:28 +0100
Subject: [PATCH] remove lemma `finite_dec`

---
 theories/finite.v | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/theories/finite.v b/theories/finite.v
index 9aac9ff0..0cd64c40 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).
-- 
GitLab