proposition: Lemma subst_forall_prv phi {N Gamma} : Gamma ⊢ (forall_times N phi) -> bounded N phi -> forall sigma, Gamma ⊢ phi[sigma].
proof: Proof. induction N in phi |-*; intros ?? sigma; cbn in *. - change sigma with (iter up 0 sigma). now rewrite (subst_bounded 0). - specialize (IHN (∀ phi) ). rewrite <-up_decompose. apply AllE. apply IHN. unfold forall_times. now rewrite <-iter_switch. now apply bounded_S_quant. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts