proposition: Lemma embed_term_correct rho rho' xO xS xA xEq t : env_contains_PA2 rho rho' xO xS xA xEq -> @eval Σf Σp D I rho t = @eval Σf' Σp' D I' rho' (embed_term xO xS xA t).
proof: Proof. intros E. induction t; cbn. - apply E. - destruct E as [_ [E2 _]]. apply map_ext_forall in IH. unfold insert in *. destruct ar as [|[|[]]]; cbn. all: try destruct Compare_dec.le_lt_dec; cbn; rewrite E2; cbn. all: try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia; try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia; now rewrite map_map, IH. - destruct E as [_ [E2 _]]. apply map_ext_forall in IH. unfold insert in *. destruct f; cbn in *; rewrite E2; destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia; try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia. all: now rewrite map_map, IH. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec