proposition: Lemma iso_env_i rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p x y : ⟨rho1_i, rho1_f, rho1_p⟩ ≈ ⟨rho2_i, rho2_f, rho2_p⟩ -> x ≈ y -> ⟨x .: rho1_i, rho1_f, rho1_p⟩ ≈ ⟨y .: rho2_i, rho2_f, rho2_p⟩.
proof: Proof. intros H1 H2. split. destruct n; firstorder. apply H1. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)