fact: Definition iso_env_funcfree (rho1 : env D1) rho2 := forall n, get_indi rho1 n ≈ get_indi rho2 n /\ forall ar, get_pred rho1 n ar ≈ get_pred rho2 n ar.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)