fact: Fixpoint funcfree (phi : SOL.form) := match phi with | atom _ v => Forall funcfreeTerm v | fal => True | bin _ phi psi => funcfree phi /\ funcfree psi | quant_indi _ phi => funcfree phi | quant_func _ ar' phi => False | quant_pred _ _ phi => funcfree phi end.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec