proposition: Lemma env_contains_PA2_scons_i rho rho' xO xS xA xEq d : env_contains_PA2 rho rho' xO xS xA xEq -> env_contains_PA2 ⟨d .: get_indi rho, get_func rho, get_pred rho⟩ ⟨d .: get_indi rho', get_func rho', get_pred rho'⟩ xO xS xA xEq.
proof: Proof. intros E. split. 2: apply E. intros []. reflexivity. apply E. 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