proposition: Lemma bounded_indi_up n m phi : m >= n -> bounded_indi n phi -> bounded_indi m phi.
proof: Proof. revert m n. induction phi; intros m n' H1 H2; cbn in *. easy. eapply Forall_ext. 2: apply H2. intros v; now apply bounded_indi_term_up. firstorder. eapply IHphi. 2: apply H2. lia. all: firstorder. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec