proposition: Lemma eval_predicate_ext rho1 rho2 ar (P : predicate ar) : (forall n ar v, get_pred rho1 n ar v <-> get_pred rho2 n ar v) -> forall v, eval_predicate rho1 P v <-> eval_predicate rho2 P v.
proof: Proof. intros H v. destruct P; cbn. apply H. reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector