proposition: Lemma iso_env_funcfree_p rho1_i rho1_f rho1_p rho2_i rho2_f rho2_p ar (P1 : vec D1 ar -> Prop) P2 : ⟨rho1_i, rho1_f, rho1_p⟩ ≈FF ⟨rho2_i, rho2_f, rho2_p⟩ -> P1 ≈ P2 -> ⟨rho1_i, rho1_f, P1 .: rho1_p⟩ ≈FF ⟨rho2_i, rho2_f, P2 .: rho2_p⟩.
proof: Proof. intros H1 H2 n. split. apply H1. intros ar'. destruct n; cbn; destruct Nat.eq_dec 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)