proposition: Lemma eval_subst_cons_shift_f (rho : env domain) ar (f : vec domain ar -> domain) t : eval rho t = eval ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ t[↑ ar]f.
proof: Proof. induction t; cbn [eval]. - reflexivity. - rewrite eval_function_subst_cons_shift_f with (g := f). cbn. f_equal. rewrite map_map. apply map_ext_forall, IH. - cbn. f_equal. rewrite map_map. apply map_ext_forall, IH. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector