proposition: Lemma eval_predicate_subst_cons_shift_p (rho : env domain) ar (P : predicate ar) ar' (Q : vec domain ar' -> Prop) : eval_predicate rho P = eval_predicate ⟨ get_indi rho, get_func rho, Q .: get_pred rho ⟩ (P[↑ ar']p).
proof: Proof. destruct P. - unfold econs, econs_pred, econs_ar, shift, shift_p; cbn. destruct Nat.eq_dec as [->|]; cbn. now destruct Nat.eq_dec. destruct n. destruct Nat.eq_dec; try easy. now destruct Nat.eq_dec. - reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector