proposition: Fact fol_def_list_fa K l (R : K -> (nat -> X) -> Prop) : (forall k, In k l -> fol_definable (R k)) -> fol_definable (fun φ => forall k, In k l -> R k φ).
proof: Proof. intros H. set (f := fun k Hk => proj1_sig (H k Hk)). exists (fol_lconj (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_lconj; split. * intros H1 k Hk; apply (proj2_sig (H k Hk)), H1. change (In (f k Hk) (list_in_map l f)). apply In_list_in_map. * intros H1 A H2. apply In_list_in_map_inv in H2. destruct H2 as (k & Hk & ->). 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)