proposition: Lemma eval_up ρ s t : eval (s .: ρ) t`[↑] = eval ρ t.
proof: Proof. rewrite eval_comp. apply eval_ext. reflexivity. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia