proposition: Lemma eval_same env trm : eval env trm = @FullCore.eval _ _ D (tarski_full_tarski_interp I) env trm.
proof: Proof. induction trm as [n|k v IH]. - easy. - destruct I. cbn. erewrite VectorSpec.map_ext_in. 1:reflexivity. apply IH. Qed.
imports: Vector Undecidability.FOL(Syntax.Facts) Undecidability.FOL.Semantics.Tarski(FullFacts FragmentFacts) Undecidability.FOL.Semantics.FiniteTarski(Full Fragment) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.Synthetic(Definitions)