fact: Definition env_equiv (rho1 : env domain) rho2 := forall n, get_indi rho1 n = get_indi rho2 n /\ forall ar v, get_func rho1 n ar v = get_func rho2 n ar v /\ (get_pred rho1 n ar v <-> get_pred rho2 n ar v).
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector