proposition: Theorem H10p_to_validity Σf Σp e : H10p e <-> forall (M : @Model Σf Σp) rho, (M, rho) ⊨ (∀f(0) ∀f(1) ∀f(2) ∀f(2) ∀p(2) (embed_form 0 0 0 0 (PA2_form ~> encode_problem e))).
proof: Proof. split. - intros H M rho. apply PA2_model_valid_iff_model_valid. apply PA2_valid_alternative. intros M' H1 rho'. now apply H10p_to_PA2_model_sat. - intros H. apply H10p_to_PA2_standard_model_sat. intros rho. apply PA2_model_valid_iff_model_valid; trivial. intros phi H1. now apply std_model_correct. 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