proposition: Lemma sat_encoding alpha rho p q : (Standard_Model, ⟨alpha, get_func rho, get_pred rho⟩) ⊨ (encode_polynomial p == encode_polynomial q) <-> dp_eval_pfree alpha p = dp_eval_pfree alpha q.
proof: Proof. split. - intros H%eq_sem. now repeat rewrite eval_encoding in H. apply std_model_correct. - intros. apply eq_sem. apply std_model_correct. now repeat rewrite eval_encoding. Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec