proposition: Lemma eval_comp_f (rho : env domain) σ t : eval rho (t[σ]f) = eval ⟨get_indi rho, σ >>> eval_function rho, get_pred rho⟩ t.
proof: Proof. induction t; cbn. reflexivity. all: 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