proposition: Lemma iso_env_f rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (f1 : vec D1 ar -> D1) f2 : ⟨rho1_i, rho1_f, rho1_p⟩ ≈ ⟨rho2_i, rho2_f, rho2_p⟩ -> f1 ≈ f2 -> ⟨rho1_i, f1 .: rho1_f, rho1_p⟩ ≈ ⟨rho2_i, f2 .: rho2_f, rho2_p⟩.
proof: Proof. intros H1 H2. split. apply H1. intros ar'. split. 2: apply H1. destruct n; cbn; destruct (PeanoNat.Nat.eq_dec ar ar') as [->|]. apply H2. all: apply H1. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)