proposition: Lemma eval_comp rho xi t : eval rho (subst_term xi t) = eval (xi >> eval rho) t.
proof: Proof. induction t; cbn. - reflexivity. - f_equal. rewrite map_map. apply map_ext_in, IH. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia