proposition: Lemma exists_n_sat phi n : first_order phi -> bounded_indi n phi -> M ⊨ exists_n n phi <-> exists rho, (M, rho) ⊨ phi.
proof: Proof. intros FO B. split. - enough (forall rho, (M, rho) ⊨ (exists_n n phi) -> exists sigma, (M, sigma) ⊨ phi) as X. { intros H. apply (X (empty_PA2_env _)), H. } revert phi FO B. induction n; intros phi FO B rho H. + now exists rho. + cbn [exists_n] in H. rewrite exists_n_switch in H. destruct (IHn (∃i phi) FO B rho H) as [sigma [x H1]]. eexists. apply H1. - intros [rho H]. revert rho phi FO B H. induction n; intros rho phi FO B H sigma. + eapply sat_ext_closed_FO; try easy. apply H. + cbn [exists_n]. rewrite exists_n_switch. apply (IHn ⟨fun n => get_indi rho (S n), get_func rho, get_pred rho⟩). apply FO. apply B. cbn. exists (get_indi rho 0). eapply sat_ext. 2: apply H. split. now induction n0. easy. 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