proposition: Lemma bounded_pred_up ar n m phi : m >= n -> bounded_pred ar n phi -> bounded_pred ar m phi.
proof: Proof. revert m n. induction phi; intros m n' H1 H2; cbn in *. easy. destruct p. lia. easy. 1-3: firstorder. destruct H2 as [H2|H2]. - left. split. easy. eapply IHphi. 2: apply H2. lia. - right. split. easy. eapply IHphi. 2: apply H2. lia. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec