proposition: Lemma bounded_S_quant {ff : falsity_flag} {q : quantop} N phi : bounded (S N) phi <-> bounded N (@quant _ _ _ _ q phi).
proof: Proof. split; intros H. - now constructor. - inversion H. apply Eqdep_dec.inj_pair2_eq_dec in H4 as ->; trivial. unfold Dec.dec. decide equality. 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