proposition: Fact fol_def_list_ex K l (R : K -> (nat -> X) -> Prop) : (forall k, In k l -> fol_definable (R k)) -> fol_definable (fun φ => exists k, In k l /\ R k φ).
proof: Proof. intros H. set (f := fun k Hk => proj1_sig (H k Hk)). exists (fol_ldisj (list_in_map l f)); msplit 2. + rewrite fol_syms_bigop. intros s; simpl; rewrite app_nil_r. rewrite in_flat_map. intros (A & H1 & H2). apply In_list_in_map_inv in H1. destruct H1 as (k & Hk & ->). revert H2; apply (proj2_sig (H k Hk)); auto. + rewrite fol_rels_bigop. intros s; simpl; rewrite app_nil_r. rewrite in_flat_map. intros (A & H1 & H2). apply In_list_in_map_inv in H1. destruct H1 as (k & Hk & ->). revert H2; apply (proj2_sig (H k Hk)); auto. + intros phi. rewrite fol_sem_ldisj; split. * intros (A & H1 & HA). apply In_list_in_map_inv in H1. destruct H1 as (k & Hk & ->). exists k; split; auto. apply (proj2_sig (H k Hk)); auto. * intros (k & Hk & H1). exists (f k Hk); split. - apply In_list_in_map. - apply (proj2_sig (H k Hk)); 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)