proposition: Lemma find_bounded_t t : { n | bounded_t n t }.
proof: Proof. Proof using Σ_preds ops. induction t using term_rect. - exists (S x). constructor. lia. - apply find_bounded_step in X as [n H]. exists n. now constructor. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts