proposition: Lemma eval_function_subst_cons_shift_f (rho : env domain) ar (f : function ar) ar' (g : vec domain ar' -> domain) : eval_function rho f = eval_function ⟨ get_indi rho, g .: get_func rho, get_pred rho ⟩ (f[↑ ar']f).
proof: Proof. destruct f. - unfold econs, econs_func, econs_ar, shift, shift_f; 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