proposition: Lemma eval_ext rho xi t : (forall x, rho x = xi x) -> eval rho t = eval xi t.
proof: Proof. intros H. induction t; cbn. - now apply H. - f_equal. apply map_ext_in. now apply IH. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia