proposition: Lemma bounded_indi_term_up n m t : m >= n -> bounded_indi_term n t -> bounded_indi_term m t.
proof: Proof. Proof using Σ_pred ops. intros H1. induction t; intros H2; cbn in *. lia. induction v; firstorder. induction v; firstorder. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec