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