proposition: Lemma env_equiv_symm rho1 rho2 : rho1 ≡ rho2 -> rho2 ≡ rho1.
proof: Proof. intros H. intros n. specialize (H n). split. easy. intros ar v. destruct H as [_ H]. specialize (H ar v). easy. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector