proposition: Theorem H10p_to_PA2_validity e : H10p e <-> PA2 ⊨ encode_problem e.
proof: Proof. split. - intros H. apply PA2_valid_alternative. intros M HM rho. now apply H10p_to_PA2_model_sat. - intros H. eapply H10p_to_PA2_model_sat with (rho := empty_PA2_env Standard_Model). apply std_model_correct. eapply PA2_valid_alternative in H. apply H. 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