fact: Definition up_p `{preds_signature} (σp : nat -> forall ar, predicate ar) ar := econs (@var_pred _ 0 ar) (fun x ar' => (σp x ar')[shift ar]p).
imports: Arith Lia Vector Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax) Undecidability.SOL.SOL