proposition: Lemma find_bounded {ff : falsity_flag} phi : { n | bounded n phi }.
proof: Proof. induction phi. - exists 0. constructor. - destruct (@find_bounded_step _ t) as [n Hn]. + eauto using find_bounded_t. + exists n. now constructor. - destruct IHphi1 as [n Hn], IHphi2 as [k Hk]. exists (n + k). constructor; eapply bounded_up; try eassumption; lia. - destruct IHphi as [n Hn]. exists n. constructor. apply (bounded_up Hn). 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