proposition: Lemma find_bounded_step n (v : vec term n) : (forall t : term, InT t v -> {n : nat | bounded_t n t}) -> { n | forall t, In t v -> bounded_t n t }.
proof: Proof. Proof using Σ_preds ops. induction v; cbn; intros HV. - exists 0. intros t. inversion 1. - destruct IHv as [k Hk], (HV h) as [l Hl]; try now left. + intros t Ht. apply HV. now right. + exists (k + l). intros t H. destruct (In_inv H) as [->|H']. * cbn. apply (bounded_up_t Hl). lia. * cbn in H'. apply (bounded_up_t (Hk t H')). lia. 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