proposition: Lemma bounded_func_term_up ar n m t : m >= n -> bounded_func_term ar n t -> bounded_func_term ar m t.
proof: Proof. intros H1. induction t; intros H2; cbn in *. easy. split. lia. eapply Forall_ext_Forall. apply IH. apply H2. eapply Forall_ext_Forall. apply IH. apply H2. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec