proposition: Lemma exists_close_form {ff : falsity_flag} N phi : bounded 0 (exist_times N phi) <-> bounded N phi.
proof: Proof. induction N in phi |- *. - reflexivity. - cbn. rewrite iter_switch. change (iter _ _ _) with (exist_times N (∃ phi)). setoid_rewrite IHN. symmetry. now apply bounded_S_quant. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia