diff --git a/theories/list.v b/theories/list.v
index c68da7b5582a812a87a250f373ed56072b5db962..1b16fbfa05729d385064d4e2ba1919e3f6daa5e1 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -939,21 +939,6 @@ Proof.
   destruct (nth_lookup_or_length l i d); [done | by lia].
 Qed.
 
-Lemma list_in_dec (P : A → Prop) (l : list A) :
-  (∀ x, Decision (P x)) →
-  Decision (∃ x, P x ∧ x ∈ l).
-Proof.
-  intros HdecP. induction l as [ | it l IH].
-  - right. intros (it & _ & []%elem_of_nil).
-  - destruct IH as [ IH | IH].
-    + left. destruct IH as (it' & Hit' & Hin).
-      exists it'. split; [done|]. right. done.
-    + destruct (HdecP it) as [Hit | Hnit].
-      { left. exists it. split; [done|]. by left. }
-      right. intros (it' & Hit' & [-> | Hin]%elem_of_cons); [done|].
-      apply IH. eauto.
-Qed.
-
 (** ** Properties of the [NoDup] predicate *)
 Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
@@ -2948,6 +2933,17 @@ Section Forall_Exists.
     end.
 End Forall_Exists.
 
+Lemma list_exist_dec P l :
+  (∀ x, Decision (P x)) → Decision (∃ x, x ∈ l ∧ P x).
+Proof.
+  refine (λ _, cast_if (decide (Exists P l))); by rewrite <-Exists_exists.
+Defined.
+Lemma list_forall_dec P l :
+  (∀ x, Decision (P x)) → Decision (∀ x, x ∈ l → P x).
+Proof.
+  refine (λ _, cast_if (decide (Forall P l))); by rewrite <-Forall_forall.
+Defined.
+
 Lemma forallb_True (f : A → bool) xs : forallb f xs ↔ Forall f xs.
 Proof.
   split.