proposition: Lemma env_equiv_cons_p rho1 rho2 ar (P : vec domain ar -> Prop) : rho1 ≡ rho2 -> ⟨ get_indi rho1, get_func rho1, P .: get_pred rho1 ⟩ ≡ ⟨ get_indi rho2, get_func rho2, P .: get_pred rho2 ⟩.
proof: Proof. intros H n. split. 2:split. - apply H. - apply H. - destruct n; cbn; destruct (Nat.eq_dec ar ar0) as [->|]. all: firstorder. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector