proposition: Lemma funcfree_bounded_func_term t : funcfreeTerm t -> forall x ar, bounded_func_term x ar t.
proof: Proof. intros F x ar. induction t; cbn in *; try easy. eapply Forall_ext_Forall. apply IH. apply F. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec