proposition: Lemma exists_n_bounded n phi : bounded_indi 0 (exists_n n phi) <-> bounded_indi n phi.
proof: Proof. induction n in phi |- *. - easy. - cbn [exists_n]. rewrite exists_n_switch. apply IHn. Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec