fact: Definition form2cform phi : cform := exist _ (exclosure phi) (exclosure_closed phi).
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Semantics.FiniteTarski.Full) Undecidability.Synthetic.Definitions Vector Lia