proposition: Lemma subst_exist_prv {sigma N Gamma} phi : Gamma ⊢ phi[sigma] -> bounded N phi -> Gamma ⊢ exist_times N phi.
proof: Proof. induction N in phi, sigma |-*; intros; cbn. - erewrite <- (subst_bounded 0); eassumption. - rewrite iter_switch. eapply (IHN (S >> sigma)). cbn. eapply (ExI (sigma 0)). now rewrite up_decompose. now apply bounded_S_quant. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia