proposition: Theorem decidable_list_upto_fa l : (forall x, exists y, In y l /\ R x y) -> decidable (forall x, P x).
proof: Proof. Proof using HR HP. intros Hl. destruct list_dec with (P := fun x => ~ P x) (Q := P) (l := l) as [ (x & H1 & H2) | H ]. + intros x; generalize (HP x); unfold decidable; tauto. + right; contradict H2; auto. + left; intros x. destruct (Hl x) as (y & H1 & H2). generalize (H _ H1); apply (HR H2). Qed.
imports: List Arith Bool Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops)