proposition: Fact fol_def_bounded_fa m (R : nat -> (nat -> X) -> Prop) : (forall n, n < m -> fol_definable (R n)) -> fol_definable (fun φ => forall n, n < m -> R n φ).
proof: Proof. intros H. apply fol_def_equiv with (R := fun φ => forall n, In n (list_an 0 m) -> R n φ). + intros phi; apply forall_equiv; intro; rewrite list_an_spec; simpl; split; try tauto. intros H1 ?; apply H1; lia. + apply fol_def_list_fa. intros n Hn; apply H; revert Hn; rewrite list_an_spec; lia. 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)