proposition: Lemma fin_dec_ex (P:D->Prop) : (forall k, dec (P k)) -> dec (exists k, P k).
proof: Proof. Proof using fini. intros HPr. assert (forall (l:list D), dec (exists k0, In k0 l /\ P k0)) as H. - intros l. induction l as [|lx lr [IHt|IHf]]. + right. intros [v [[] _]]. + left. destruct IHt as [d [Hdl Hdr]]. exists d. split; firstorder. + destruct (HPr lx) as [Ht|Hf]. * left. exists lx. split; firstorder. * right. intros [v [[->|vlr] Pv]]. 1:easy. apply IHf. exists v. now split. - destruct fini as [l Hl]. destruct (H l) as [Ht|Hf]. + left. destruct Ht as [d [_ Pd]]. now exists d. + right. intros [d Pd]. apply Hf. exists d. split. 2:easy. apply Hl. Defined.
imports: Undecidability.FOL.Semantics(Tarski.FragmentFacts) Undecidability.FOL.Syntax(Facts) Undecidability.Synthetic.DecidabilityFacts Undecidability.Synthetic.EnumerabilityFacts Undecidability.Shared.Dec List