proposition: Fact fol_def_finite_ex I (R : I -> (nat -> X) -> Prop) : finite_t I -> (forall i, fol_definable ls lr M (R i)) -> fol_definable ls lr M (fun φ => exists i : I, R i φ).
proof: Proof. intros (l & Hl) H. apply fol_def_equiv with (R := fun φ => exists i, In i l /\ R i φ). + intros phi; apply exists_equiv; intro; split; auto; tauto. + apply fol_def_list_ex; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic)