proposition: Lemma exists_n_sat_2 rho phi n : (M, rho) ⊨ (exists_n n phi) -> first_order phi -> bounded_indi n phi -> exists sigma, (M, sigma) ⊨ phi.
proof: Proof. intros. eapply exists_n_sat; eauto. intros sigma. eapply sat_ext_closed_FO. now apply exists_n_first_order. now apply exists_n_bounded. eassumption. Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec