proposition: Lemma fin_dec (P:D->Prop) : (forall k, dec (P k)) -> dec (forall k, P k).
proof: Proof. Proof using fini. intros HPr. assert (forall (l:list D), dec (forall k0, In k0 l -> P k0)) as H. - intros l. induction l as [|lx lr [IHt|IHf]]. + left. intros v []. + destruct (HPr lx) as [Ht|Hf]. * left. intros h. intros [l|r]. 1:congruence. now apply IHt. * right. intros Hc. apply Hf, Hc. now left. + right. intros Hc. apply IHf. intros k Hk. apply Hc. now right. - destruct fini as [l Hl]. destruct (H l) as [Ht|Hf]. + left. intros k. apply Ht, Hl. + right. intros Hc. apply Hf. intros k Hk. apply Hc. Defined.
imports: Undecidability.FOL.Semantics(Tarski.FragmentFacts) Undecidability.FOL.Syntax(Facts) Undecidability.Synthetic.DecidabilityFacts Undecidability.Synthetic.EnumerabilityFacts Undecidability.Shared.Dec List