proposition: Lemma embed_form_correct rho rho' xO xS xA xEq phi : env_contains_PA2 rho rho' xO xS xA xEq -> @sat Σf Σp D I rho phi <-> @sat Σf' Σp' D I' rho' (embed_form xO xS xA xEq phi).
proof: Proof. revert rho rho' xO xS xA xEq. induction phi; intros rho rho' xO xS xA xEq E; cbn. - reflexivity. - rename t into v. assert (map (@eval Σf Σp D I rho) v = map (fun t => @eval Σf' Σp' D I' rho' (embed_term xO xS xA t)) v) as Hv'. { clear p. induction v. reflexivity. cbn; f_equal. apply (embed_term_correct _ _ _ _ _ _ _ E). apply IHv. } destruct E as [_ [_ E3]]. destruct p; cbn. + unfold insert in *. destruct ar as [|[|[]]]; try destruct Compare_dec.le_lt_dec; cbn; rewrite E3; try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia; now rewrite map_map, Hv'. + unfold insert in *. destruct P; cbn in *. rewrite E3. destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia. now rewrite map_map, Hv'. - specialize (IHphi1 rho rho' xO xS xA xEq E); specialize (IHphi2 rho rho' xO xS xA xEq E). destruct b; tauto. - destruct q. + split; intros H d; eapply IHphi. 2,4: apply (H d). all: now apply env_contains_PA2_scons_i. + split; intros [d H]; exists d; eapply IHphi. 2,4: apply H. all: now apply env_contains_PA2_scons_i. - destruct q; destruct n as [|[|[]]]; split. 1-8: intros H f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA2_scons_f f). all: intros [f H]; exists f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA2_scons_f f). - destruct q; destruct n as [|[|[]]]; split. 1-8: intros H P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA2_scons_p P). all: intros [P H]; exists P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA2_scons_p P). 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