proposition: Lemma exclosure_closed phi : bounded 0 (exclosure phi).
proof: Proof. unfold exclosure. destruct find_bounded as [N HN]. now apply exists_close_form. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Semantics.FiniteTarski.Full) Undecidability.Synthetic.Definitions Vector Lia