fact: Definition exclosure phi : form := let (N, _) := find_bounded phi in exist_times N phi.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Semantics.FiniteTarski.Full) Undecidability.Synthetic.Definitions Vector Lia