proposition: Lemma eval_function_ext rho1 rho2 ar (f : function ar) : (forall n ar v, get_func rho1 n ar v = get_func rho2 n ar v) -> forall v, eval_function rho1 f v = eval_function rho2 f v.
proof: Proof. intros H v. destruct f; cbn. apply H. reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector