fact: Fixpoint cast {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off := match phi with | falsity => Q | atom P v => (@atom _ _ _ falsity_off (old_preds P) v) | bin b phi psi => bin b (cast phi) (cast psi) | quant q phi => quant q (cast phi) end.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FragmentSyntax)