proposition: Lemma find_bounded_L {ff : falsity_flag} A : { n | bounded_L n A }.
proof: Proof. induction A; cbn. - exists 0. intros phi. inversion 1. - destruct IHA as [k Hk], (find_bounded a) as [l Hl]. exists (k + l). intros t [<-|H]; eapply bounded_up; try eassumption; try (now apply Hk); 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