proposition: Lemma subst_bounded_max {ff : falsity_flag} n m phi sigma : (forall i, i < n -> bounded_t m (sigma i)) -> bounded n phi -> bounded m (phi[sigma]).
proof: Proof. intros Hi. induction 1 as [ff n P v H| bo ff n phi psi H1 IH1 H2 IH2| qo ff n phi H1 IH1| n] in Hi,sigma,m|-*; cbn; econstructor. - intros t [x [Hx <-]]%vector_in_map. eapply subst_bounded_max_t. 1: exact Hi. now apply H. - apply IH1. easy. - apply IH2. easy. - apply IH1. intros l Hl. apply subst_bounded_up_t. intros i' Hi'. apply Hi. lia. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts