proposition: Lemma subst_exist_sat {ff : falsity_flag} rho phi N : rho ⊨ phi -> bounded N phi -> forall rho, rho ⊨ (exist_times N phi).
proof: Proof. induction N in phi, rho |-*; intros. - cbn. eapply sat_closed; eassumption. - cbn -[sat]. rewrite iter_switch. apply (IHN (S >> rho)). exists (rho 0). eapply sat_ext. 2: apply H. now intros []. now apply bounded_S_quant. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia