proposition: Fact exists_list_sem_dec X (P : X -> Prop) (l : list X) : (forall x, { P x } + { ~ P x }) -> { exists x, In x l /\ P x } + { ~ exists x, In x l /\ P x }.
proof: Proof. intros H. destruct list_dec with (P := P) (Q := fun x => ~ P x) (l := l) as [ (x & H1 & H2) | H1 ]; auto. + left; firstorder. + right; intros (y & Hy). apply (H1 y); tauto. Qed.
imports: List Arith Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)